Merge branch 'master' of github.com:diffblue/cbmc

kroening · kroening · commit 2a95e59c3528 · 2017-03-23T08:50:15.000Z
diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -8,6 +8,5 @@ main.c
 ^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$
 ^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
 ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
-
 ^\*\* 2 of 6 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -6,6 +6,5 @@ main.c
 ^\[main.assertion.2\] assertion y: FAILURE$
 ^\[main.assertion.3\] assertion z1: SUCCESS$
 ^\[main.assertion.4\] assertion z2: SUCCESS$
-
 ^\*\* 1 of 4 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-copy/test.desc b/regression/cbmc/Quantifiers-copy/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion b\[.*\] == 2: SUCCESS$
 ^\[main.assertion.4\] assertion b\[.*\] == 3: SUCCESS$
 ^\[main.assertion.5\] assertion b\[.*\] == 4: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] success 1: SUCCESS$
 ^\[main.assertion.4\] failure 3: FAILURE$
 ^\[main.assertion.5\] success 2: SUCCESS$
-
 ^\*\* 3 of 5 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-initialisation/test.desc b/regression/cbmc/Quantifiers-initialisation/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\] == 3: SUCCESS$
 ^\[main.assertion.4\] assertion a\[.*\] == 4: SUCCESS$
 ^\[main.assertion.5\] assertion a\[.*\] == 5: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\] > a\[.*\]: FAILURE$
 ^\[main.assertion.4\] forall c\[\]: SUCCESS$
 ^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
-
 ^\*\* 1 of 5 failed \(2 iterations\)$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
@@ -2,6 +2,5 @@ CORE
 main.c
 
 ^\*\* Results:$
-
 ^\*\* 0 of 1 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc
@@ -8,6 +8,5 @@ main.c
 ^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$
 ^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$
 ^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
-
 ^\*\* 0 of 6 failed \(1 iteration\)$
 ^\VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] failure 1: FAILURE$
 ^\[main.assertion.4\] success 3: SUCCESS$
 ^\[main.assertion.5\] failure 2: FAILURE$
-
 ^\*\* 2 of 5 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
 ^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc
@@ -4,6 +4,5 @@ main.c
 ^\*\* Results:$
 ^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
 ^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
-
 ^\*\* 1 of 2 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile
@@ -1,10 +1,16 @@
 default: tests.log
 
 test:
-	@../test.pl -c ../../../src/goto-analyzer/goto-analyzer
+	@if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 tests.log: ../test.pl
-	@../test.pl -c ../../../src/goto-analyzer/goto-analyzer
+	@if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 show:
 	@for dir in *; do \
diff --git a/regression/test-script/excluded-line/program.c b/regression/test-script/excluded-line/program.c
diff --git a/regression/test-script/excluded-line/test.desc b/regression/test-script/excluded-line/test.desc
@@ -1,5 +1,5 @@
 CORE
-program.c
+test.txt
 
 ^Hello$
 --
diff --git a/regression/test-script/excluded-line/test.txt b/regression/test-script/excluded-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/failing-excluded-line/program.c b/regression/test-script/failing-excluded-line/program.c
diff --git a/regression/test-script/failing-excluded-line/test.desc b/regression/test-script/failing-excluded-line/test.desc
@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 ^Hello$
 --
diff --git a/regression/test-script/failing-excluded-line/test.txt b/regression/test-script/failing-excluded-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/failing-multi-line/program.c b/regression/test-script/failing-multi-line/program.c
diff --git a/regression/test-script/failing-multi-line/test.desc b/regression/test-script/failing-multi-line/test.desc
@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 activate-multi-line-match
 Hello\nAnother\nWorld
diff --git a/regression/test-script/failing-multi-line/test.txt b/regression/test-script/failing-multi-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/failing-single-line/program.c b/regression/test-script/failing-single-line/program.c
diff --git a/regression/test-script/failing-single-line/test.desc b/regression/test-script/failing-single-line/test.desc
@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 ^Goodbye$
 --
diff --git a/regression/test-script/failing-single-line/test.txt b/regression/test-script/failing-single-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/multi-line/program.c b/regression/test-script/multi-line/program.c
diff --git a/regression/test-script/multi-line/test.desc b/regression/test-script/multi-line/test.desc
@@ -1,5 +1,5 @@
 CORE
-program.c
+test.txt
 
 activate-multi-line-match
 Hello\nWorld
diff --git a/regression/test-script/multi-line/test.txt b/regression/test-script/multi-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/program_runner.sh b/regression/test-script/program_runner.sh
@@ -2,5 +2,4 @@
 
 set -e
 
-gcc $1 -o a.out
-./a.out
+cat $1
diff --git a/regression/test-script/single-line-windows-line-ends/test.desc b/regression/test-script/single-line-windows-line-ends/test.desc
@@ -0,0 +1,5 @@
+CORE
+test.txt
+
+^Hello$
+--
diff --git a/regression/test-script/single-line-windows-line-ends/test.txt b/regression/test-script/single-line-windows-line-ends/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/single-line/program.c b/regression/test-script/single-line/program.c
diff --git a/regression/test-script/single-line/test.desc b/regression/test-script/single-line/test.desc
@@ -1,5 +1,5 @@
 CORE
-program.c
+test.txt
 
 ^Hello$
 --
diff --git a/regression/test-script/single-line/test.txt b/regression/test-script/single-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test.pl b/regression/test.pl
@@ -73,7 +73,7 @@ ($$$$$)
   $options =~ s/$ign//g if(defined($ign));
 
   my $output = $input;
-  $output =~ s/\.(c|i|gb|cpp|ii|xml|class|jar)$/.out/;
+  $output =~ s/\.[^.]*$/.out/;
 
   if($output eq $input) {
     print("Error in test file -- $test\n");
@@ -125,13 +125,15 @@ ($$$$$)
             local $/ = undef;
             binmode $fh;
             my $whole_file = <$fh>;
+            $whole_file =~ s/\r\n/\n/g;
             my $is_match = $whole_file =~ /$result/;
             $r = ($included ? !$is_match : $is_match);
           }
           else
           {
             my $found_line = 0;
             while(my $line = <$fh>) {
+              $line =~ s/\r$//;
               if($line =~ /$result/) {
                 # We've found the line, therefore if it is included we set
                 # the result to 0 (OK) If it is excluded, we set the result
diff --git a/scripts/cpplint.py b/scripts/cpplint.py
@@ -1145,6 +1145,7 @@ def RepositoryName(self):
             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
diff --git a/scripts/filter_lint_by_diff.py b/scripts/filter_lint_by_diff.py
@@ -8,11 +8,11 @@
   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 @@
       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)
diff --git a/scripts/run_lint.sh b/scripts/run_lint.sh
@@ -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" ]
diff --git a/src/util/file_util.cpp b/src/util/file_util.cpp
