results now include line number

kroening · kroening · commit 5cb389be2d61 · 2018-11-04T13:58:20.000Z
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
