Skip to content

Commit 2a95e59

Browse files
author
Daniel Kroening
committed
Merge branch 'master' of github.com:diffblue/cbmc
2 parents c21d3ed + ff9d833 commit 2a95e59

File tree

38 files changed

+105
-97
lines changed

38 files changed

+105
-97
lines changed

regression/cbmc/Quantifiers-assertion/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,5 @@ main.c
88
^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$
99
^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
1010
^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
11-
1211
^\*\* 2 of 6 failed \(2 iterations\)$
1312
^\VERIFICATION FAILED$

regression/cbmc/Quantifiers-assignment/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,5 @@ main.c
66
^\[main.assertion.2\] assertion y: FAILURE$
77
^\[main.assertion.3\] assertion z1: SUCCESS$
88
^\[main.assertion.4\] assertion z2: SUCCESS$
9-
109
^\*\* 1 of 4 failed \(2 iterations\)$
1110
^\VERIFICATION FAILED$

regression/cbmc/Quantifiers-copy/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,5 @@ main.c
77
^\[main.assertion.3\] assertion b\[.*\] == 2: SUCCESS$
88
^\[main.assertion.4\] assertion b\[.*\] == 3: SUCCESS$
99
^\[main.assertion.5\] assertion b\[.*\] == 4: SUCCESS$
10-
1110
^\*\* 0 of 5 failed \(1 iteration\)$
1211
^VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-if/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,5 @@ main.c
77
^\[main.assertion.3\] success 1: SUCCESS$
88
^\[main.assertion.4\] failure 3: FAILURE$
99
^\[main.assertion.5\] success 2: SUCCESS$
10-
1110
^\*\* 3 of 5 failed \(2 iterations\)$
1211
^\VERIFICATION FAILED$

regression/cbmc/Quantifiers-initialisation/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,5 @@ main.c
77
^\[main.assertion.3\] assertion a\[.*\] == 3: SUCCESS$
88
^\[main.assertion.4\] assertion a\[.*\] == 4: SUCCESS$
99
^\[main.assertion.5\] assertion a\[.*\] == 5: SUCCESS$
10-
1110
^\*\* 0 of 5 failed \(1 iteration\)$
1211
^VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-initialisation2/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,5 @@ main.c
77
^\[main.assertion.3\] assertion a\[.*\] > a\[.*\]: FAILURE$
88
^\[main.assertion.4\] forall c\[\]: SUCCESS$
99
^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
10-
1110
^\*\* 1 of 5 failed \(2 iterations\)$
1211
^VERIFICATION FAILED$

regression/cbmc/Quantifiers-invalid-var-range/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,5 @@ CORE
22
main.c
33

44
^\*\* Results:$
5-
65
^\*\* 0 of 1 failed \(1 iteration\)$
76
^VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-not-exists/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,5 @@ main.c
88
^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$
99
^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$
1010
^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
11-
1211
^\*\* 0 of 6 failed \(1 iteration\)$
1312
^\VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-not/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,5 @@ main.c
77
^\[main.assertion.3\] failure 1: FAILURE$
88
^\[main.assertion.4\] success 3: SUCCESS$
99
^\[main.assertion.5\] failure 2: FAILURE$
10-
1110
^\*\* 2 of 5 failed \(2 iterations\)$
1211
^\VERIFICATION FAILED$

regression/cbmc/Quantifiers-two-dimension-array/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,5 @@ main.c
77
^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
88
^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
99
^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$
10-
1110
^\*\* 0 of 5 failed \(1 iteration\)$
1211
^VERIFICATION SUCCESSFUL$

regression/cbmc/Quantifiers-type/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,5 @@ main.c
44
^\*\* Results:$
55
^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
66
^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
7-
87
^\*\* 1 of 2 failed \(2 iterations\)$
98
^\VERIFICATION FAILED$

regression/goto-analyzer/Makefile

+8-2
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,16 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -c ../../../src/goto-analyzer/goto-analyzer
4+
@if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \
5+
../failed-tests-printer.pl ; \
6+
exit 1 ; \
7+
fi
58

69
tests.log: ../test.pl
7-
@../test.pl -c ../../../src/goto-analyzer/goto-analyzer
10+
@if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \
11+
../failed-tests-printer.pl ; \
12+
exit 1 ; \
13+
fi
814

915
show:
1016
@for dir in *; do \

regression/test-script/excluded-line/program.c

-7
This file was deleted.

regression/test-script/excluded-line/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
CORE
2-
program.c
2+
test.txt
33

44
^Hello$
55
--
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Hello
2+
World
3+

regression/test-script/failing-excluded-line/program.c

-7
This file was deleted.

regression/test-script/failing-excluded-line/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
KNOWNBUG
2-
program.c
2+
test.txt
33

44
^Hello$
55
--
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Hello
2+
World
3+

regression/test-script/failing-multi-line/program.c

-7
This file was deleted.

regression/test-script/failing-multi-line/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
KNOWNBUG
2-
program.c
2+
test.txt
33

44
activate-multi-line-match
55
Hello\nAnother\nWorld
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Hello
2+
World
3+

regression/test-script/failing-single-line/program.c

-7
This file was deleted.

regression/test-script/failing-single-line/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
KNOWNBUG
2-
program.c
2+
test.txt
33

44
^Goodbye$
55
--
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Hello
2+
World
3+

regression/test-script/multi-line/program.c

-7
This file was deleted.

regression/test-script/multi-line/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
CORE
2-
program.c
2+
test.txt
33

44
activate-multi-line-match
55
Hello\nWorld
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Hello
2+
World
3+

regression/test-script/program_runner.sh

+1-2
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,4 @@
22

33
set -e
44

5-
gcc $1 -o a.out
6-
./a.out
5+
cat $1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
CORE
2+
test.txt
3+
4+
^Hello$
5+
--
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Hello
2+
World
3+

regression/test-script/single-line/program.c

-7
This file was deleted.
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
CORE
2-
program.c
2+
test.txt
33

44
^Hello$
55
--
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Hello
2+
World
3+

regression/test.pl

+3-1
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ ($$$$$)
7373
$options =~ s/$ign//g if(defined($ign));
7474

7575
my $output = $input;
76-
$output =~ s/\.(c|i|gb|cpp|ii|xml|class|jar)$/.out/;
76+
$output =~ s/\.[^.]*$/.out/;
7777

7878
if($output eq $input) {
7979
print("Error in test file -- $test\n");
@@ -125,13 +125,15 @@ ($$$$$)
125125
local $/ = undef;
126126
binmode $fh;
127127
my $whole_file = <$fh>;
128+
$whole_file =~ s/\r\n/\n/g;
128129
my $is_match = $whole_file =~ /$result/;
129130
$r = ($included ? !$is_match : $is_match);
130131
}
131132
else
132133
{
133134
my $found_line = 0;
134135
while(my $line = <$fh>) {
136+
$line =~ s/\r$//;
135137
if($line =~ /$result/) {
136138
# We've found the line, therefore if it is included we set
137139
# the result to 0 (OK) If it is excluded, we set the result

scripts/cpplint.py

+1
Original file line numberDiff line numberDiff line change
@@ -1145,6 +1145,7 @@ def RepositoryName(self):
11451145
os.path.exists(os.path.join(current_dir, ".hg")) or
11461146
os.path.exists(os.path.join(current_dir, ".svn"))):
11471147
root_dir = current_dir
1148+
break;
11481149
current_dir = os.path.dirname(current_dir)
11491150

11501151
if (os.path.exists(os.path.join(root_dir, ".git")) or

scripts/filter_lint_by_diff.py

+10-9
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,11 @@
88
print >>sys.stderr, "Usage: filter_lint_by_diff.py diff.patch repository_root_directory < cpplint_warnings.txt"
99
sys.exit(1)
1010

11-
added_lines = set()
1211
repository_root = sys.argv[2]
1312

14-
diff = unidiff.PatchSet.from_filename(sys.argv[1])
15-
for diff_file in diff:
13+
# Create a set of all the files and the specific lines within that file that are in the diff
14+
added_lines = set()
15+
for diff_file in unidiff.PatchSet.from_filename(sys.argv[1]):
1616
filename = diff_file.target_file
1717
# Skip files deleted in the tip (b side of the diff):
1818
if filename == "/dev/null":
@@ -25,11 +25,12 @@
2525
if diff_line.line_type == "+":
2626
added_lines.add((filename, diff_line.target_line_no))
2727

28-
for l in sys.stdin:
29-
bits = l.split(":")
30-
if len(bits) < 3:
28+
# Print the lines that are in the set
29+
for line in sys.stdin:
30+
line_parts = line.split(":")
31+
if len(line_parts) < 3:
3132
continue
32-
filename = os.path.join(repository_root, bits[0])
33-
linenum = int(bits[1])
33+
filename = os.path.join(repository_root, line_parts[0])
34+
linenum = int(line_parts[1])
3435
if (filename, linenum) in added_lines:
35-
sys.stdout.write(l)
36+
sys.stdout.write(line)

scripts/run_lint.sh

+9-2
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
set -e
44

55
script_folder=`dirname $0`
6-
absolute_repository_root=`readlink -f $script_folder/..`
6+
absolute_repository_root=`git rev-parse --show-toplevel`
77

88
if [[ "$#" -gt 2 ]]
99
then
@@ -20,6 +20,13 @@ then
2020
exit 1
2121
fi
2222

23+
if ! [[ -e $script_folder/filter_lint_by_diff.py ]]
24+
then
25+
echo "Lint filter script could not be found in the $script_folder directory"
26+
echo "Ensure filter_lint_by_diff.py is inside the $script_folder directory then run again"
27+
exit 1
28+
fi
29+
2330
if [[ "$#" -gt 0 ]]
2431
then
2532
git_start=$1
@@ -62,7 +69,7 @@ for file in $diff_files; do
6269

6370
# Run the linting script and filter:
6471
# The errors from the linter go to STDERR so must be redirected to STDOUT
65-
result=`$script_folder/cpplint.py $file 2>&1 | $script_folder/filter_lint_by_diff.py $diff_file $absolute_repository_root`
72+
result=`$script_folder/cpplint.py $file 2>&1 >/dev/null | $script_folder/filter_lint_by_diff.py $diff_file $absolute_repository_root`
6673

6774
# Providing some errors were relevant we print them out
6875
if [ "$result" ]

0 commit comments

Comments
 (0)