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

results now include line number

This commit is contained in:
Daniel Kroening 2018-11-04 13:57:56 +00:00
parent 3028bf8bf8
commit 73c33841b7
44 changed files with 153 additions and 145 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
jbmc/regression/jbmc/catch1/test.desc
View File

@ -4,6 +4,6 @@ catch1.class
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
^\[.*\] no uncaught exception: FAILURE$
^\[.*\] line 15 no uncaught exception: FAILURE$
--
^warning: ignoring

2
jbmc/regression/jbmc/temp_stack_variable_packing/test.desc
View File

@ -1,7 +1,7 @@
CORE
Primary.class
--function Primary.main
^\[java::Primary.Run:\(\)V\.assertion\.1\] assertion at file Primary\.java line 6 function java::Primary.Run:\(\)V bytecode-index 22: FAILURE$
^\[java::Primary.Run:\(\)V\.assertion\.1\] line 6 assertion at file Primary\.java line 6 function java::Primary.Run:\(\)V bytecode-index 22: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring

2
regression/cbmc/Array_operations1/test.desc
View File

@ -3,7 +3,7 @@ main.c
^EXIT=10$
^SIGNAL=0$
^\[test_copy\.assertion\.4\] expected to fail: FAILURE$
^\[test_copy\.assertion\.4\] .* expected to fail: FAILURE$
^\*\* 1 of 8 failed
^VERIFICATION FAILED$
--

2
regression/cbmc/Function5/test.desc
View File

@ -3,6 +3,6 @@ main.c
--pointer-check --bounds-check
^SIGNAL=0$
^EXIT=10$
^\[.*\] dereference failure: pointer outside object bounds in \*p: FAILURE$
^\[.*\] .* dereference failure: pointer outside object bounds in \*p: FAILURE$
--
^warning: ignoring

4
regression/cbmc/Multi_Dimensional_Array6/test.desc
View File

@ -3,8 +3,8 @@ main.c
--unwind 3 --no-unwinding-assertions
^EXIT=10$
^SIGNAL=0$
^\[main\.assertion\.1\] : SUCCESS$
^\[main\.assertion\.2\] : FAILURE$
^\[main\.assertion\.1\] .* : SUCCESS$
^\[main\.assertion\.2\] .* : FAILURE$
^\*\* 1 of 2 failed
--
^warning: ignoring

2
regression/cbmc/Multiple_Properties1/test.desc
View File

@ -5,6 +5,6 @@ activate-multi-line-match
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
^main.c function main\n\[main\.assertion\.1\] .* SUCCESS\n\[main\.assertion\.3\] .* FAILURE$
^main.c function main\n\[main\.assertion\.1\] line 5 .* SUCCESS\n\[main\.assertion\.3\] line 9 .* FAILURE$
--
^warning: ignoring

2
regression/cbmc/Overflow_Addition1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--signed-overflow-check
^EXIT=10$
^SIGNAL=0$
^\[.*\] arithmetic overflow on signed \+ in .*: FAILURE$
^\[.*\] .* arithmetic overflow on signed \+ in .*: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring

2
regression/cbmc/Overflow_Leftshift1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--signed-overflow-check
^EXIT=10$
^SIGNAL=0$
^\[.*\] arithmetic overflow on signed shl in .*: FAILURE$
^\[.*\] .* arithmetic overflow on signed shl in .*: FAILURE$
^\*\* 2 of 4 failed
^VERIFICATION FAILED$
--

12
regression/cbmc/Quantifiers-assertion/test.desc
View File

@ -2,12 +2,12 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] Exists-Exists: successful: SUCCESS$
^\[main.assertion.2\] NotExists-NotExists: successful: SUCCESS$
^\[main.assertion.3\] NotExists-Exists: failed: FAILURE$
^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$
^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
^\[main.assertion.1\] .* Exists-Exists: successful: SUCCESS$
^\[main.assertion.2\] .* NotExists-NotExists: successful: SUCCESS$
^\[main.assertion.3\] .* NotExists-Exists: failed: FAILURE$
^\[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
^VERIFICATION FAILED$
^EXIT=10$

8
regression/cbmc/Quantifiers-assignment/test.desc
View File

@ -2,10 +2,10 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] assertion x: SUCCESS$
^\[main.assertion.2\] assertion y: FAILURE$
^\[main.assertion.3\] assertion z1: SUCCESS$
^\[main.assertion.4\] assertion z2: SUCCESS$
^\[main.assertion.1\] .* assertion x: SUCCESS$
^\[main.assertion.2\] .* assertion y: FAILURE$
^\[main.assertion.3\] .* assertion z1: SUCCESS$
^\[main.assertion.4\] .* assertion z2: SUCCESS$
^\*\* 1 of 4 failed
^VERIFICATION FAILED$
^EXIT=10$

10
regression/cbmc/Quantifiers-copy/test.desc
View File

@ -2,11 +2,11 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] assertion b\[.*\] == 0: SUCCESS$
^\[main.assertion.2\] assertion b\[.*\] == 1: SUCCESS$
^\[main.assertion.3\] assertion b\[.*\] == 2: SUCCESS$
^\[main.assertion.4\] assertion b\[.*\] == 3: SUCCESS$
^\[main.assertion.5\] assertion b\[.*\] == 4: SUCCESS$
^\[main.assertion.1\] .* assertion b\[.*\] == 0: SUCCESS$
^\[main.assertion.2\] .* assertion b\[.*\] == 1: SUCCESS$
^\[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
^VERIFICATION SUCCESSFUL$
^EXIT=0$

10
regression/cbmc/Quantifiers-if/test.desc
View File

@ -2,11 +2,11 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] failure 1: FAILURE$
^\[main.assertion.2\] failure 2: FAILURE$
^\[main.assertion.3\] success 1: SUCCESS$
^\[main.assertion.4\] failure 3: FAILURE$
^\[main.assertion.5\] success 2: SUCCESS$
^\[main.assertion.1\] .* failure 1: FAILURE$
^\[main.assertion.2\] .* failure 2: FAILURE$
^\[main.assertion.3\] .* success 1: SUCCESS$
^\[main.assertion.4\] .* failure 3: FAILURE$
^\[main.assertion.5\] .* success 2: SUCCESS$
^\*\* 3 of 5 failed
^VERIFICATION FAILED$
^EXIT=10$

10
regression/cbmc/Quantifiers-initialisation/test.desc
View File

@ -2,11 +2,11 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] assertion a\[.*\] == 1: SUCCESS$
^\[main.assertion.2\] assertion a\[.*\] == 2: SUCCESS$
^\[main.assertion.3\] assertion a\[.*\] == 3: SUCCESS$
^\[main.assertion.4\] assertion a\[.*\] == 4: SUCCESS$
^\[main.assertion.5\] assertion a\[.*\] == 5: SUCCESS$
^\[main.assertion.1\] .* assertion a\[.*\] == 1: SUCCESS$
^\[main.assertion.2\] .* assertion a\[.*\] == 2: SUCCESS$
^\[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
^VERIFICATION SUCCESSFUL$
^EXIT=0$

10
regression/cbmc/Quantifiers-initialisation2/test.desc
View File

@ -2,11 +2,11 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] forall a\[\]: SUCCESS$
^\[main.assertion.2\] assertion a\[.*\] > a\[.*\]: SUCCESS$
^\[main.assertion.3\] assertion a\[.*\] > a\[.*\]: FAILURE$
^\[main.assertion.4\] forall c\[\]: SUCCESS$
^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
^\[main.assertion.1\] .* forall a\[\]: SUCCESS$
^\[main.assertion.2\] .* assertion a\[.*\] > a\[.*\]: SUCCESS$
^\[main.assertion.3\] .* assertion a\[.*\] > a\[.*\]: FAILURE$
^\[main.assertion.4\] .* forall c\[\]: SUCCESS$
^\[main.assertion.5\] .* assertion c\[.*\] >= c\[.*\]: SUCCESS$
^\*\* 1 of 5 failed
^VERIFICATION FAILED$
^EXIT=10$

12
regression/cbmc/Quantifiers-not-exists/test.desc
View File

@ -2,12 +2,12 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] assertion a\[.*\]\[.*\] > 10: SUCCESS$
^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.3\] assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.4\] assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.6\] assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.1\] line 18 assertion a\[.*\]\[.*\] > 10: SUCCESS$
^\[main.assertion.2\] line 20 assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.3\] line 21 assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.4\] line 23 assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.5\] line 25 assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.6\] line 26 assertion tmp_if_expr\$\d+: SUCCESS$
^\*\* 0 of 6 failed
^VERIFICATION SUCCESSFUL$
^EXIT=0$

10
regression/cbmc/Quantifiers-not/test.desc
View File

@ -2,11 +2,11 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] success 1: SUCCESS$
^\[main.assertion.2\] success 2: SUCCESS$
^\[main.assertion.3\] failure 1: FAILURE$
^\[main.assertion.4\] success 3: SUCCESS$
^\[main.assertion.5\] failure 2: FAILURE$
^\[main.assertion.1\] .* success 1: SUCCESS$
^\[main.assertion.2\] .* success 2: SUCCESS$
^\[main.assertion.3\] .* failure 1: FAILURE$
^\[main.assertion.4\] .* success 3: SUCCESS$
^\[main.assertion.5\] .* failure 2: FAILURE$
^\*\* 2 of 5 failed
^VERIFICATION FAILED$
^EXIT=10$

10
regression/cbmc/Quantifiers-two-dimension-array/test.desc
View File

@ -2,11 +2,11 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] assertion a\[.*\]\[.*\] == 0: SUCCESS$
^\[main.assertion.2\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.1\] line 9 assertion a\[.*\]\[.*\] == 0: SUCCESS$
^\[main.assertion.2\] line 10 assertion a\[.*\]\[.*\] == 1: SUCCESS$
^\[main.assertion.3\] line 11 assertion a\[.*\]\[.*\] == 1: SUCCESS$
^\[main.assertion.4\] line 12 assertion a\[.*\]\[.*\] == 2: SUCCESS$
^\[main.assertion.5\] line 13 assertion tmp_if_expr\$\d+: SUCCESS$
^\*\* 0 of 5 failed
^VERIFICATION SUCCESSFUL$
^EXIT=0$

4
regression/cbmc/Quantifiers-type/test.desc
View File

@ -2,8 +2,8 @@ CORE
main.c
^\*\* Results:$
^\[main.assertion.1\] assertion tmp_if_expr(\$\d+)?: FAILURE$
^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$
^\[main.assertion.1\] line 9 assertion tmp_if_expr(\$\d+)?: FAILURE$
^\[main.assertion.2\] line 10 assertion tmp_if_expr\$\d+: SUCCESS$
^\*\* 1 of 2 failed
^VERIFICATION FAILED$
^EXIT=10$

2
regression/cbmc/Undefined_Shift1/test.desc
View File

@ -3,7 +3,7 @@ main.c
--undefined-shift-check
^EXIT=10$
^SIGNAL=0$
^\[.*\] shift operand is negative in .*: FAILURE$
^\[.*\] line 8 shift operand is negative in .*: FAILURE$
^\*\* 1 of 2 failed
^VERIFICATION FAILED$
--

2
regression/cbmc/fgets1/test.desc
View File

@ -4,7 +4,7 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
\[main.assertion.3\] assertion p\[1\]=='b': FAILURE
\[main.assertion.3\] line 16 assertion p\[1\]=='b': FAILURE
\*\* 2 of \d+ failed
--
^warning: ignoring

4
regression/cbmc/gcc_bswap1/test.desc
View File

@ -4,8 +4,8 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
\[main\.assertion\.[258]\] assertion __builtin_bswap(16|32|64)\((sb|b|bl)\) == 0: FAILURE$
\[main\.assertion\.[258]\] .* assertion __builtin_bswap(16|32|64)\((sb|b|bl)\) == 0: FAILURE$
^\*\* 3 of 9 failed
--
^warning: ignoring
\[main\.assertion\.[258]\] assertion __builtin_bswap(16|32|64)\((sb|b|bl)\) == 0: SUCCESS$
\[main\.assertion\.[258]\] .* assertion __builtin_bswap(16|32|64)\((sb|b|bl)\) == 0: SUCCESS$

2
regression/cbmc/goto4/test.desc
View File

@ -3,7 +3,7 @@ main.c
--unwind 1 --unwinding-assertions
^EXIT=10$
^SIGNAL=0$
^\[.*] assertion g == 0: SUCCESS$
^\[.*] line 5 assertion g == 0: SUCCESS$
^\[.*] unwinding assertion loop 0: FAILURE$
--
^warning: ignoring

2
regression/cbmc/memcpy1/test.desc
View File

@ -4,7 +4,7 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
^\[main\.precondition_instance\..*\] memcpy source region readable: FAILURE$
^\[main\.precondition_instance\..*\] .* memcpy source region readable: FAILURE$
\*\* 1 of [0-9]+ failed
--
^warning: ignoring

8
regression/cbmc/memory_allocation1/test.desc
View File

@ -3,10 +3,10 @@ main.c
--pointer-check
^EXIT=10$
^SIGNAL=0$
^\[main\.pointer_dereference\.2\] dereference failure: invalid integer address in \*p: SUCCESS$
^\[main\.assertion\.1\] assertion \*p==42: SUCCESS$
^\[main\.pointer_dereference\.[0-9]+\] dereference failure: invalid integer address in p\[.*1\]: FAILURE$
^\[main\.assertion\.2\] assertion \*\(p\+1\)==42: SUCCESS$
^\[main\.pointer_dereference\.2\] .* dereference failure: invalid integer address in \*p: SUCCESS$
^\[main\.assertion\.1\] .* assertion \*p==42: SUCCESS$
^\[main\.pointer_dereference\.[0-9]+\] .* dereference failure: invalid integer address in p\[.*1\]: FAILURE$
^\[main\.assertion\.2\] .* assertion \*\(p\+1\)==42: SUCCESS$
^VERIFICATION FAILED$
--
^warning: ignoring

2
regression/cbmc/memset1/test.desc
View File

@ -4,7 +4,7 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
^\[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE$
^\[main.assertion.7\] .* assertion A\[1\]==0x01010111: FAILURE$
\*\* 1 of [0-9]+ failed
--
^warning: ignoring

2
regression/cbmc/memset3/test.desc
View File

@ -4,7 +4,7 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
^\[main\.precondition_instance\..*] memset destination region writeable: FAILURE$
^\[main\.precondition_instance\..*] .* memset destination region writeable: FAILURE$
\*\* 1 of [0-9]+ failed \(.*\)
--
^warning: ignoring

2
regression/cbmc/pipe1/test.desc
View File

@ -3,7 +3,7 @@ main.c
^EXIT=10$
^SIGNAL=0$
^\[main\.assertion\.4\] assertion data\[1\]==31: FAILURE$
^\[main\.assertion\.4\] .* assertion data\[1\]==31: FAILURE$
^\*\* 1 of 5 failed
--
^warning: ignoring

56
regression/cbmc/pointer-extra-checks/test.desc
View File

@ -3,37 +3,37 @@ main.c
--pointer-check
^EXIT=10$
^SIGNAL=0$
^\[main.pointer_dereference.1\] dereference failure: pointer NULL in \*p: FAILURE$
^\[main.pointer_dereference.2\] dereference failure: dead object in \*q: SUCCESS$
^\[main.pointer_dereference.3\] dereference failure: pointer outside object bounds in \*q: SUCCESS$
^\[main.pointer_dereference.4\] dereference failure: deallocated dynamic object in \*r: SUCCESS$
^\[main.pointer_dereference.5\] dereference failure: pointer outside dynamic object bounds in \*r: SUCCESS$
^\[main.pointer_dereference.6\] dereference failure: pointer uninitialized in \*s: FAILURE$
^\[main.pointer_dereference.1\] .* dereference failure: pointer NULL in \*p: FAILURE$
^\[main.pointer_dereference.2\] .* dereference failure: dead object in \*q: SUCCESS$
^\[main.pointer_dereference.3\] .* dereference failure: pointer outside object bounds in \*q: SUCCESS$
^\[main.pointer_dereference.4\] .* dereference failure: deallocated dynamic object in \*r: SUCCESS$
^\[main.pointer_dereference.5\] .* dereference failure: pointer outside dynamic object bounds in \*r: SUCCESS$
^\[main.pointer_dereference.6\] .* dereference failure: pointer uninitialized in \*s: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*p:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer uninitialized in \*p:
^\[main.pointer_dereference.[0-9]+\] dereference failure: deallocated dynamic object in \*p:
^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*p:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside dynamic object bounds in \*p:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*p:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer NULL in \*q:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*q:
^\[main.pointer_dereference.[0-9]+\] dereference failure: deallocated dynamic object in \*q:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside dynamic object bounds in \*q:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer uninitialized in \*q:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer NULL in \*r:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*r:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer uninitialized in \*r:
^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*r:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*r:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer NULL in \*s:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*s:
^\[main.pointer_dereference.[0-9]+\] dereference failure: deallocated dynamic object in \*s:
^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*s:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside dynamic object bounds in \*s:
^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*s:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer invalid in \*p:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer uninitialized in \*p:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: deallocated dynamic object in \*p:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: dead object in \*p:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside dynamic object bounds in \*p:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside object bounds in \*p:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer NULL in \*q:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer invalid in \*q:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: deallocated dynamic object in \*q:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside dynamic object bounds in \*q:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer uninitialized in \*q:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer NULL in \*r:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer invalid in \*r:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer uninitialized in \*r:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: dead object in \*r:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside object bounds in \*r:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer NULL in \*s:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer invalid in \*s:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: deallocated dynamic object in \*s:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: dead object in \*s:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside dynamic object bounds in \*s:
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside object bounds in \*s:
--
This test ensures that local_bitvector_analysis is correctly labelling obvious
cases of pointers and that --pointer-check is not generating excess assertions.

2
regression/cbmc/read1/test.desc
View File

@ -4,7 +4,7 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
\[.*] dereference failure: pointer outside object bounds in .*: FAILURE
\[.*] .* dereference failure: pointer outside object bounds in .*: FAILURE
\*\* 1 of .* failed \(.*\)
--
^warning: ignoring

4
regression/cbmc/return2/test.desc
View File

@ -4,8 +4,8 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
\[main.assertion..\] expected to fail: FAILURE$
\[main.assertion..\] .* expected to fail: FAILURE$
\*\* 2 of 2 failed
--
^warning: ignoring
\[main.assertion..\] expected to fail: SUCCESS$
\[main.assertion..\] .* expected to fail: SUCCESS$

2
regression/cbmc/strcat1/test.desc
View File

@ -4,7 +4,7 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
\[main.assertion.6\] assertion strlen\(A3\) == 4: FAILURE
\[main.assertion.6\] .* assertion strlen\(A3\) == 4: FAILURE
\*\* 1 of 9 failed
--
^warning: ignoring

4
regression/contracts/function_check_04/test.desc
View File

@ -1,8 +1,8 @@
CORE
main.c
--apply-code-contracts
^\[main.assertion.1\] assertion x == 0: SUCCESS$
^\[foo.1\] : FAILURE$
^\[main.assertion.1\] .* assertion x == 0: SUCCESS$
^\[foo.1\] line 9 : FAILURE$
^VERIFICATION FAILED$
--
--

6
regression/contracts/invar_check_04/test.desc
View File

@ -1,9 +1,9 @@
CORE
main.c
--apply-code-contracts
^\[main.1\] Loop invariant violated before entry: SUCCESS$
^\[main.2\] Loop invariant not preserved: SUCCESS$
^\[main.assertion.1\] assertion r == 0: FAILURE$
^\[main.1\] .* Loop invariant violated before entry: SUCCESS$
^\[main.2\] .* Loop invariant not preserved: SUCCESS$
^\[main.assertion.1\] .* assertion r == 0: FAILURE$
^VERIFICATION FAILED$
--
--

4
regression/goto-instrument/generate-function-body-assert-false-assume-false/test.desc
View File

@ -4,5 +4,5 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
^\[main.assertion.1\] assertion 0: SUCCESS$
^\[crashes_program.assertion.1\] assertion false: FAILURE$
^\[main.assertion.1\] .* assertion 0: SUCCESS$
^\[crashes_program.assertion.1\] .* assertion false: FAILURE$

2
regression/goto-instrument/generate-function-body-assert-false/test.desc
View File

@ -3,6 +3,6 @@ main.c
--generate-function-body do_not_call_this --generate-function-body-options assert-false
^EXIT=10$
^SIGNAL=0$
^\[do_not_call_this.assertion.1\] assertion false: FAILURE$
^\[do_not_call_this.assertion.1\] .* assertion false: FAILURE$
--
^warning: ignoring

22
regression/goto-instrument/generate-function-body-complex-struct/test.desc
View File

@ -3,15 +3,15 @@ main.c
--generate-function-body 'havoc_complex_struct' --generate-function-body-options 'havoc,params:.*'
^SIGNAL=0$
^EXIT=10$
\[main.assertion.1\] assertion main_struct.pointer_contents->struct_contents.some_variable == 11: SUCCESS
\[main.assertion.2\] assertion main_struct.struct_contents.some_variable == 10: SUCCESS
\[main.assertion.3\] assertion main_struct.struct_contents.some_constant == 20: SUCCESS
\[main.assertion.4\] assertion main_struct.union_contents.some_double < 14.0 && main_struct.union_contents.some_double > 12.0: SUCCESS
\[main.assertion.5\] assertion main_struct.pointer_contents->struct_contents.some_variable == 11: FAILURE
\[main.assertion.6\] assertion main_struct.struct_contents.some_variable == 10: FAILURE
\[main.assertion.7\] assertion main_struct.struct_contents.some_constant == 20: SUCCESS
\[main.assertion.8\] assertion main_struct.union_contents.some_double < 14.0 && main_struct.union_contents.some_double > 12.0: FAILURE
\[main.assertion.9\] assertion child_struct.struct_contents.some_variable == 11: SUCCESS
\[main.assertion.10\] assertion child_struct.union_contents.some_integer == 31: SUCCESS
\[main.assertion.11\] assertion !child_struct.pointer_contents: SUCCESS
\[main.assertion.1\] .* assertion main_struct.pointer_contents->struct_contents.some_variable == 11: SUCCESS
\[main.assertion.2\] .* assertion main_struct.struct_contents.some_variable == 10: SUCCESS
\[main.assertion.3\] .* assertion main_struct.struct_contents.some_constant == 20: SUCCESS
\[main.assertion.4\] .* assertion main_struct.union_contents.some_double < 14.0 && main_struct.union_contents.some_double > 12.0: SUCCESS
\[main.assertion.5\] .* assertion main_struct.pointer_contents->struct_contents.some_variable == 11: FAILURE
\[main.assertion.6\] .* assertion main_struct.struct_contents.some_variable == 10: FAILURE
\[main.assertion.7\] .* assertion main_struct.struct_contents.some_constant == 20: SUCCESS
\[main.assertion.8\] .* assertion main_struct.union_contents.some_double < 14.0 && main_struct.union_contents.some_double > 12.0: FAILURE
\[main.assertion.9\] .* assertion child_struct.struct_contents.some_variable == 11: SUCCESS
\[main.assertion.10\] .* assertion child_struct.union_contents.some_integer == 31: SUCCESS
\[main.assertion.11\] .* assertion !child_struct.pointer_contents: SUCCESS
^VERIFICATION FAILED$

2
regression/goto-instrument/generate-function-body-const-pointer-to-non-const/test.desc
View File

@ -3,5 +3,5 @@ main.c
--generate-function-body change_pointer_target_of_const_pointer --generate-function-body-options havoc,params:.*
^EXIT=10$
^SIGNAL=0$
^\[main.assertion.1\] assertion x == 10: FAILURE$
^\[main.assertion.1\] .* assertion x == 10: FAILURE$
--

4
regression/goto-instrument/generate-function-body-havoc-globals/test.desc
View File

@ -4,7 +4,7 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
^\[main.assertion.1\] assertion global == 10: FAILURE$
^\[main.assertion.2\] assertion constant_global == 10: SUCCESS$
^\[main.assertion.1\] .* assertion global == 10: FAILURE$
^\[main.assertion.2\] .* assertion constant_global == 10: SUCCESS$
--
^warning: ignoring

4
regression/goto-instrument/generate-function-body-havoc-params/test.desc
View File

@ -4,7 +4,7 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
^\[main.assertion.1\] assertion parameter == 10: FAILURE$
^\[main.assertion.2\] assertion constant_parameter == 10: SUCCESS$
^\[main.assertion.1\] .* assertion parameter == 10: FAILURE$
^\[main.assertion.2\] .* assertion constant_parameter == 10: SUCCESS$
--
^warning: ignoring

6
regression/goto-instrument/generate-function-body-pointer-to-pointer-to-const/test.desc
View File

@ -3,7 +3,7 @@ main.c
--generate-function-body change_target_of_pointer_to_pointer_to_const --generate-function-body-options havoc,params:.*
^EXIT=10$
^SIGNAL=0$
^\[main.assertion.1\] assertion \*px == 10: SUCCESS$
^\[main.assertion.2\] assertion x == 10: SUCCESS$
^\[main.assertion.3\] assertion \*px == 10: FAILURE$
^\[main.assertion.1\] .* assertion \*px == 10: SUCCESS$
^\[main.assertion.2\] .* assertion x == 10: SUCCESS$
^\[main.assertion.3\] .* assertion \*px == 10: FAILURE$
--

8
regression/goto-instrument/generate-function-body-struct-with-const-member/test.desc
View File

@ -3,8 +3,8 @@ main.c
--generate-function-body 'havoc_struct' --generate-function-body-options 'havoc,params:.*,globals:(?!__).*'
^SIGNAL=0$
^EXIT=10$
^\[main.assertion.1\] assertion globalStruct.non_const == 10: FAILURE$
^\[main.assertion.2\] assertion globalStruct.is_const == 20: SUCCESS$
^\[main.assertion.3\] assertion paramStruct.non_const == 11: FAILURE$
^\[main.assertion.4\] assertion paramStruct.is_const == 21: SUCCESS$
^\[main.assertion.1\] .* assertion globalStruct.non_const == 10: FAILURE$
^\[main.assertion.2\] .* assertion globalStruct.is_const == 20: SUCCESS$
^\[main.assertion.3\] .* assertion paramStruct.non_const == 11: FAILURE$
^\[main.assertion.4\] .* assertion paramStruct.is_const == 21: SUCCESS$
^VERIFICATION FAILED$

16
regression/goto-instrument/generate-function-body-union-with-const-member/test.desc
View File

@ -3,12 +3,12 @@ main.c
--generate-function-body 'havoc_union' --generate-function-body-options 'havoc,params:.*,globals:(?!__).*'
^SIGNAL=0$
^EXIT=10$
^\[main.assertion.1\] assertion globalUnion.non_const == 10: SUCCESS$
^\[main.assertion.2\] assertion globalUnion.is_const == 10: SUCCESS$
^\[main.assertion.3\] assertion paramUnion.non_const == 20: SUCCESS$
^\[main.assertion.4\] assertion paramUnion.is_const == 20: SUCCESS$
^\[main.assertion.5\] assertion globalUnion.non_const == 10: FAILURE$
^\[main.assertion.6\] assertion globalUnion.is_const == 10: FAILURE$
^\[main.assertion.7\] assertion paramUnion.non_const == 20: FAILURE$
^\[main.assertion.8\] assertion paramUnion.is_const == 20: FAILURE$
^\[main.assertion.1\] .* assertion globalUnion.non_const == 10: SUCCESS$
^\[main.assertion.2\] .* assertion globalUnion.is_const == 10: SUCCESS$
^\[main.assertion.3\] .* assertion paramUnion.non_const == 20: SUCCESS$
^\[main.assertion.4\] .* assertion paramUnion.is_const == 20: SUCCESS$
^\[main.assertion.5\] .* assertion globalUnion.non_const == 10: FAILURE$
^\[main.assertion.6\] .* assertion globalUnion.is_const == 10: FAILURE$
^\[main.assertion.7\] .* assertion paramUnion.non_const == 20: FAILURE$
^\[main.assertion.8\] .* assertion paramUnion.is_const == 20: FAILURE$
^VERIFICATION FAILED$

4
regression/goto-instrument/generate-function-body/test.desc
View File

@ -4,5 +4,5 @@ main.c
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
^\[main.assertion.1\] assertion does_not_get_reached: SUCCESS$
^\[should_be_generated.assertion.1\] assertion false: FAILURE$
^\[main.assertion.1\] .* assertion does_not_get_reached: SUCCESS$
^\[should_be_generated.assertion.1\] .* assertion false: FAILURE$

12
src/cbmc/all_properties.cpp
View File

@ -187,6 +187,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
// now show in the order we have determined
irep_idt previous_function;
irep_idt current_file;
for(const auto &g : goals)
{
const auto &l = g->second.source_location;
@ -198,8 +199,9 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
previous_function = l.get_function();
if(!previous_function.empty())
{
if(!l.get_file().empty())
result() << l.get_file() << ' ';
current_file = l.get_file();
if(!current_file.empty())
result() << current_file << ' ';
if(!l.get_function().empty())
result() << "function " << l.get_function();
result() << eom;
@ -208,6 +210,12 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
result() << faint << '[' << g->first << "] " << reset;
if(l.get_file() != current_file)
result() << "file " << l.get_file() << ' ';
if(!l.get_line().empty())
result() << "line " << l.get_line() << ' ';
result() << g->second.description << ": ";
if(g->second.status == goalt::statust::SUCCESS)