diff --git a/jbmc/regression/jbmc/catch1/test.desc b/jbmc/regression/jbmc/catch1/test.desc index ddfa132953f..c07c2715000 100644 --- a/jbmc/regression/jbmc/catch1/test.desc +++ b/jbmc/regression/jbmc/catch1/test.desc @@ -4,6 +4,6 @@ catch1.class ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\[.*\] no uncaught exception: FAILURE$ +^\[.*\] line 15 no uncaught exception: FAILURE$ -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/temp_stack_variable_packing/test.desc b/jbmc/regression/jbmc/temp_stack_variable_packing/test.desc index 19d1488e68e..9a2c49b2f3c 100644 --- a/jbmc/regression/jbmc/temp_stack_variable_packing/test.desc +++ b/jbmc/regression/jbmc/temp_stack_variable_packing/test.desc @@ -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 diff --git a/regression/cbmc/Array_operations1/test.desc b/regression/cbmc/Array_operations1/test.desc index 2bbe617db7a..0b0aa0f57d5 100644 --- a/regression/cbmc/Array_operations1/test.desc +++ b/regression/cbmc/Array_operations1/test.desc @@ -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$ -- diff --git a/regression/cbmc/Function5/test.desc b/regression/cbmc/Function5/test.desc index 3dada8790af..d877a4247fb 100644 --- a/regression/cbmc/Function5/test.desc +++ b/regression/cbmc/Function5/test.desc @@ -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 diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc index a0a32880488..050f2fd2d15 100644 --- a/regression/cbmc/Multi_Dimensional_Array6/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array6/test.desc @@ -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 diff --git a/regression/cbmc/Multiple_Properties1/test.desc b/regression/cbmc/Multiple_Properties1/test.desc index 37817de2447..beb36b219c7 100644 --- a/regression/cbmc/Multiple_Properties1/test.desc +++ b/regression/cbmc/Multiple_Properties1/test.desc @@ -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 diff --git a/regression/cbmc/Overflow_Addition1/test.desc b/regression/cbmc/Overflow_Addition1/test.desc index 979e031e3f8..2615a9d290d 100644 --- a/regression/cbmc/Overflow_Addition1/test.desc +++ b/regression/cbmc/Overflow_Addition1/test.desc @@ -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 diff --git a/regression/cbmc/Overflow_Leftshift1/test.desc b/regression/cbmc/Overflow_Leftshift1/test.desc index 85c5de77e74..da481b5cb6d 100644 --- a/regression/cbmc/Overflow_Leftshift1/test.desc +++ b/regression/cbmc/Overflow_Leftshift1/test.desc @@ -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$ -- diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc index 018411f7345..8f2e25b3d90 100644 --- a/regression/cbmc/Quantifiers-assertion/test.desc +++ b/regression/cbmc/Quantifiers-assertion/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc index 41148962905..d9183316f55 100644 --- a/regression/cbmc/Quantifiers-assignment/test.desc +++ b/regression/cbmc/Quantifiers-assignment/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-copy/test.desc b/regression/cbmc/Quantifiers-copy/test.desc index e6138e282c0..8b1083602d9 100644 --- a/regression/cbmc/Quantifiers-copy/test.desc +++ b/regression/cbmc/Quantifiers-copy/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc index 92ad6e0bb93..76bb5083f90 100644 --- a/regression/cbmc/Quantifiers-if/test.desc +++ b/regression/cbmc/Quantifiers-if/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-initialisation/test.desc b/regression/cbmc/Quantifiers-initialisation/test.desc index 3dfc3721b41..f11fe701a7a 100644 --- a/regression/cbmc/Quantifiers-initialisation/test.desc +++ b/regression/cbmc/Quantifiers-initialisation/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc index 760a1c959e9..5bc13a1a52d 100644 --- a/regression/cbmc/Quantifiers-initialisation2/test.desc +++ b/regression/cbmc/Quantifiers-initialisation2/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc index b7181ece960..3de92781b61 100644 --- a/regression/cbmc/Quantifiers-not-exists/test.desc +++ b/regression/cbmc/Quantifiers-not-exists/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc index 884b944ec24..d853d107258 100644 --- a/regression/cbmc/Quantifiers-not/test.desc +++ b/regression/cbmc/Quantifiers-not/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc index b588f1621aa..fb34f594248 100644 --- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc +++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc @@ -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$ diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc index ba904aec101..7e7eb754d52 100644 --- a/regression/cbmc/Quantifiers-type/test.desc +++ b/regression/cbmc/Quantifiers-type/test.desc @@ -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$ diff --git a/regression/cbmc/Undefined_Shift1/test.desc b/regression/cbmc/Undefined_Shift1/test.desc index 8e4d9120b06..eaecdf381b9 100644 --- a/regression/cbmc/Undefined_Shift1/test.desc +++ b/regression/cbmc/Undefined_Shift1/test.desc @@ -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$ -- diff --git a/regression/cbmc/fgets1/test.desc b/regression/cbmc/fgets1/test.desc index 61f9a401bdb..f398db0edd5 100644 --- a/regression/cbmc/fgets1/test.desc +++ b/regression/cbmc/fgets1/test.desc @@ -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 diff --git a/regression/cbmc/gcc_bswap1/test.desc b/regression/cbmc/gcc_bswap1/test.desc index 816eb3a838b..2f839efe54a 100644 --- a/regression/cbmc/gcc_bswap1/test.desc +++ b/regression/cbmc/gcc_bswap1/test.desc @@ -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$ diff --git a/regression/cbmc/goto4/test.desc b/regression/cbmc/goto4/test.desc index 3fcce676021..961ee72a83b 100644 --- a/regression/cbmc/goto4/test.desc +++ b/regression/cbmc/goto4/test.desc @@ -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 diff --git a/regression/cbmc/memcpy1/test.desc b/regression/cbmc/memcpy1/test.desc index 611ab02bbce..0fc3b7df6f1 100644 --- a/regression/cbmc/memcpy1/test.desc +++ b/regression/cbmc/memcpy1/test.desc @@ -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 diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc index 1d4973cc324..77c4e0af53a 100644 --- a/regression/cbmc/memory_allocation1/test.desc +++ b/regression/cbmc/memory_allocation1/test.desc @@ -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 diff --git a/regression/cbmc/memset1/test.desc b/regression/cbmc/memset1/test.desc index 601660aa402..db4ec3e73bf 100644 --- a/regression/cbmc/memset1/test.desc +++ b/regression/cbmc/memset1/test.desc @@ -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 diff --git a/regression/cbmc/memset3/test.desc b/regression/cbmc/memset3/test.desc index 1f8018852c5..be58134bdcb 100644 --- a/regression/cbmc/memset3/test.desc +++ b/regression/cbmc/memset3/test.desc @@ -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 diff --git a/regression/cbmc/pipe1/test.desc b/regression/cbmc/pipe1/test.desc index 3c4aa9c5bc4..be5948c1de3 100644 --- a/regression/cbmc/pipe1/test.desc +++ b/regression/cbmc/pipe1/test.desc @@ -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 diff --git a/regression/cbmc/pointer-extra-checks/test.desc b/regression/cbmc/pointer-extra-checks/test.desc index e327a672f85..6e81aa60034 100644 --- a/regression/cbmc/pointer-extra-checks/test.desc +++ b/regression/cbmc/pointer-extra-checks/test.desc @@ -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. diff --git a/regression/cbmc/read1/test.desc b/regression/cbmc/read1/test.desc index eb5d74e7f28..9742dea8a0c 100644 --- a/regression/cbmc/read1/test.desc +++ b/regression/cbmc/read1/test.desc @@ -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 diff --git a/regression/cbmc/return2/test.desc b/regression/cbmc/return2/test.desc index d383de8d1c9..b655b34a10f 100644 --- a/regression/cbmc/return2/test.desc +++ b/regression/cbmc/return2/test.desc @@ -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$ diff --git a/regression/cbmc/strcat1/test.desc b/regression/cbmc/strcat1/test.desc index 3d8e8e421dc..0db35c7134d 100644 --- a/regression/cbmc/strcat1/test.desc +++ b/regression/cbmc/strcat1/test.desc @@ -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 diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc index db7ee5aa32a..20a7e46f099 100644 --- a/regression/contracts/function_check_04/test.desc +++ b/regression/contracts/function_check_04/test.desc @@ -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$ -- -- diff --git a/regression/contracts/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc index 7414b7f58a6..f8abcf720a5 100644 --- a/regression/contracts/invar_check_04/test.desc +++ b/regression/contracts/invar_check_04/test.desc @@ -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$ -- -- diff --git a/regression/goto-instrument/generate-function-body-assert-false-assume-false/test.desc b/regression/goto-instrument/generate-function-body-assert-false-assume-false/test.desc index dc23de4238c..1e241b84ba3 100644 --- a/regression/goto-instrument/generate-function-body-assert-false-assume-false/test.desc +++ b/regression/goto-instrument/generate-function-body-assert-false-assume-false/test.desc @@ -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$ diff --git a/regression/goto-instrument/generate-function-body-assert-false/test.desc b/regression/goto-instrument/generate-function-body-assert-false/test.desc index eb93c062a86..ffc806674b2 100644 --- a/regression/goto-instrument/generate-function-body-assert-false/test.desc +++ b/regression/goto-instrument/generate-function-body-assert-false/test.desc @@ -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 diff --git a/regression/goto-instrument/generate-function-body-complex-struct/test.desc b/regression/goto-instrument/generate-function-body-complex-struct/test.desc index ca9175398e3..24289e470a2 100644 --- a/regression/goto-instrument/generate-function-body-complex-struct/test.desc +++ b/regression/goto-instrument/generate-function-body-complex-struct/test.desc @@ -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$ diff --git a/regression/goto-instrument/generate-function-body-const-pointer-to-non-const/test.desc b/regression/goto-instrument/generate-function-body-const-pointer-to-non-const/test.desc index a3777b0ff39..e171d1d3922 100644 --- a/regression/goto-instrument/generate-function-body-const-pointer-to-non-const/test.desc +++ b/regression/goto-instrument/generate-function-body-const-pointer-to-non-const/test.desc @@ -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$ -- diff --git a/regression/goto-instrument/generate-function-body-havoc-globals/test.desc b/regression/goto-instrument/generate-function-body-havoc-globals/test.desc index 2b516e3a273..2615697e8b9 100644 --- a/regression/goto-instrument/generate-function-body-havoc-globals/test.desc +++ b/regression/goto-instrument/generate-function-body-havoc-globals/test.desc @@ -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 diff --git a/regression/goto-instrument/generate-function-body-havoc-params/test.desc b/regression/goto-instrument/generate-function-body-havoc-params/test.desc index 19d9d05976d..8ea5d8f8e20 100644 --- a/regression/goto-instrument/generate-function-body-havoc-params/test.desc +++ b/regression/goto-instrument/generate-function-body-havoc-params/test.desc @@ -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 diff --git a/regression/goto-instrument/generate-function-body-pointer-to-pointer-to-const/test.desc b/regression/goto-instrument/generate-function-body-pointer-to-pointer-to-const/test.desc index 7df3009a3ed..93e9a645372 100644 --- a/regression/goto-instrument/generate-function-body-pointer-to-pointer-to-const/test.desc +++ b/regression/goto-instrument/generate-function-body-pointer-to-pointer-to-const/test.desc @@ -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$ -- diff --git a/regression/goto-instrument/generate-function-body-struct-with-const-member/test.desc b/regression/goto-instrument/generate-function-body-struct-with-const-member/test.desc index 68a7e35e8e7..d8879d2edf1 100644 --- a/regression/goto-instrument/generate-function-body-struct-with-const-member/test.desc +++ b/regression/goto-instrument/generate-function-body-struct-with-const-member/test.desc @@ -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$ diff --git a/regression/goto-instrument/generate-function-body-union-with-const-member/test.desc b/regression/goto-instrument/generate-function-body-union-with-const-member/test.desc index 726ddc45c4a..9fea290b7aa 100644 --- a/regression/goto-instrument/generate-function-body-union-with-const-member/test.desc +++ b/regression/goto-instrument/generate-function-body-union-with-const-member/test.desc @@ -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$ diff --git a/regression/goto-instrument/generate-function-body/test.desc b/regression/goto-instrument/generate-function-body/test.desc index d61fa11dc44..f9e0afbfd79 100644 --- a/regression/goto-instrument/generate-function-body/test.desc +++ b/regression/goto-instrument/generate-function-body/test.desc @@ -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$ diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 20d00cdea1c..4f5048b8268 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -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)