replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #648 from NathanJPhillips/bugfix/lint-work-across-repos 

Bugfix/lint infrastructure improvements
This commit is contained in:
Vojtěch Forejt 2017-03-21 15:04:02 +00:00 committed by GitHub
parent a7663cb997 36dee831ad
commit d4d44db701
3 changed files with 20 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
scripts/cpplint.py vendored
View File

@ -1145,6 +1145,7 @@ class FileInfo(object):
os.path.exists(os.path.join(current_dir, ".hg")) or
os.path.exists(os.path.join(current_dir, ".svn"))):
root_dir = current_dir
break;
current_dir = os.path.dirname(current_dir)
if (os.path.exists(os.path.join(root_dir, ".git")) or

19
scripts/filter_lint_by_diff.py
View File

@ -8,11 +8,11 @@ if len(sys.argv) != 3:
print >>sys.stderr, "Usage: filter_lint_by_diff.py diff.patch repository_root_directory < cpplint_warnings.txt"
sys.exit(1)
added_lines = set()
repository_root = sys.argv[2]
diff = unidiff.PatchSet.from_filename(sys.argv[1])
for diff_file in diff:
# Create a set of all the files and the specific lines within that file that are in the diff
added_lines = set()
for diff_file in unidiff.PatchSet.from_filename(sys.argv[1]):
filename = diff_file.target_file
# Skip files deleted in the tip (b side of the diff):
if filename == "/dev/null":
@ -25,11 +25,12 @@ for diff_file in diff:
if diff_line.line_type == "+":
added_lines.add((filename, diff_line.target_line_no))
for l in sys.stdin:
bits = l.split(":")
if len(bits) < 3:
# Print the lines that are in the set
for line in sys.stdin:
line_parts = line.split(":")
if len(line_parts) < 3:
continue
filename = os.path.join(repository_root, bits[0])
linenum = int(bits[1])
filename = os.path.join(repository_root, line_parts[0])
linenum = int(line_parts[1])
if (filename, linenum) in added_lines:
sys.stdout.write(l)
sys.stdout.write(line)

11
scripts/run_lint.sh
View File

@ -3,7 +3,7 @@
set -e
script_folder=`dirname $0`
absolute_repository_root=`readlink -f $script_folder/..`
absolute_repository_root=`git rev-parse --show-toplevel`
if [[ "$#" -gt 2 ]]
then
@ -20,6 +20,13 @@ then
exit 1
fi
if ! [[ -e $script_folder/filter_lint_by_diff.py ]]
then
echo "Lint filter script could not be found in the $script_folder directory"
echo "Ensure filter_lint_by_diff.py is inside the $script_folder directory then run again"
exit 1
fi
if [[ "$#" -gt 0 ]]
then
git_start=$1
@ -62,7 +69,7 @@ for file in $diff_files; do
# Run the linting script and filter:
# The errors from the linter go to STDERR so must be redirected to STDOUT
result=`$script_folder/cpplint.py $file 2>&1 | $script_folder/filter_lint_by_diff.py $diff_file $absolute_repository_root`
result=`$script_folder/cpplint.py $file 2>&1 >/dev/null | $script_folder/filter_lint_by_diff.py $diff_file $absolute_repository_root`
# Providing some errors were relevant we print them out
if [ "$result" ]