Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion regression/cbmc/Quantifiers-assertion/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
1 change: 0 additions & 1 deletion regression/cbmc/Quantifiers-assignment/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
1 change: 0 additions & 1 deletion regression/cbmc/Quantifiers-copy/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
1 change: 0 additions & 1 deletion regression/cbmc/Quantifiers-if/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
1 change: 0 additions & 1 deletion regression/cbmc/Quantifiers-initialisation/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
1 change: 0 additions & 1 deletion regression/cbmc/Quantifiers-initialisation2/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
1 change: 0 additions & 1 deletion regression/cbmc/Quantifiers-invalid-var-range/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,5 @@ CORE
main.c

^\*\* Results:$

^\*\* 0 of 1 failed \(1 iteration\)$
^VERIFICATION SUCCESSFUL$
1 change: 0 additions & 1 deletion regression/cbmc/Quantifiers-not-exists/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
1 change: 0 additions & 1 deletion regression/cbmc/Quantifiers-not/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
1 change: 0 additions & 1 deletion regression/cbmc/Quantifiers-two-dimension-array/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
1 change: 0 additions & 1 deletion regression/cbmc/Quantifiers-type/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
10 changes: 8 additions & 2 deletions regression/goto-analyzer/Makefile
Original file line number Diff line number Diff line change
@@ -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 \
Expand Down
7 changes: 0 additions & 7 deletions regression/test-script/excluded-line/program.c

This file was deleted.

2 changes: 1 addition & 1 deletion regression/test-script/excluded-line/test.desc
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
CORE
program.c
test.txt

^Hello$
--
Expand Down
3 changes: 3 additions & 0 deletions regression/test-script/excluded-line/test.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Hello
World

7 changes: 0 additions & 7 deletions regression/test-script/failing-excluded-line/program.c

This file was deleted.

2 changes: 1 addition & 1 deletion regression/test-script/failing-excluded-line/test.desc
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
KNOWNBUG
program.c
test.txt

^Hello$
--
Expand Down
3 changes: 3 additions & 0 deletions regression/test-script/failing-excluded-line/test.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Hello
World

7 changes: 0 additions & 7 deletions regression/test-script/failing-multi-line/program.c

This file was deleted.

2 changes: 1 addition & 1 deletion regression/test-script/failing-multi-line/test.desc
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
KNOWNBUG
program.c
test.txt

activate-multi-line-match
Hello\nAnother\nWorld
Expand Down
3 changes: 3 additions & 0 deletions regression/test-script/failing-multi-line/test.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Hello
World

7 changes: 0 additions & 7 deletions regression/test-script/failing-single-line/program.c

This file was deleted.

2 changes: 1 addition & 1 deletion regression/test-script/failing-single-line/test.desc
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
KNOWNBUG
program.c
test.txt

^Goodbye$
--
Expand Down
3 changes: 3 additions & 0 deletions regression/test-script/failing-single-line/test.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Hello
World

7 changes: 0 additions & 7 deletions regression/test-script/multi-line/program.c

This file was deleted.

2 changes: 1 addition & 1 deletion regression/test-script/multi-line/test.desc
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
CORE
program.c
test.txt

activate-multi-line-match
Hello\nWorld
Expand Down
3 changes: 3 additions & 0 deletions regression/test-script/multi-line/test.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Hello
World

3 changes: 1 addition & 2 deletions regression/test-script/program_runner.sh
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,4 @@

set -e

gcc $1 -o a.out
./a.out
cat $1
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
CORE
test.txt

^Hello$
--
3 changes: 3 additions & 0 deletions regression/test-script/single-line-windows-line-ends/test.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Hello
World

7 changes: 0 additions & 7 deletions regression/test-script/single-line/program.c

This file was deleted.

2 changes: 1 addition & 1 deletion regression/test-script/single-line/test.desc
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
CORE
program.c
test.txt

^Hello$
--
3 changes: 3 additions & 0 deletions regression/test-script/single-line/test.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Hello
World

4 changes: 3 additions & 1 deletion regression/test.pl
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand Down Expand Up @@ -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
Expand Down