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
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/catch1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 1 addition & 1 deletion jbmc/regression/jbmc/temp_stack_variable_packing/test.desc
Original file line number Diff line number Diff line change
@@ -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 changes: 1 addition & 1 deletion regression/cbmc/Array_operations1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
--
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Function5/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 2 additions & 2 deletions regression/cbmc/Multi_Dimensional_Array6/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 1 addition & 1 deletion regression/cbmc/Multiple_Properties1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 1 addition & 1 deletion regression/cbmc/Overflow_Addition1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 1 addition & 1 deletion regression/cbmc/Overflow_Leftshift1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
--
Expand Down
12 changes: 6 additions & 6 deletions regression/cbmc/Quantifiers-assertion/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
Expand Down
8 changes: 4 additions & 4 deletions regression/cbmc/Quantifiers-assignment/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
Expand Down
10 changes: 5 additions & 5 deletions regression/cbmc/Quantifiers-copy/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
Expand Down
10 changes: 5 additions & 5 deletions regression/cbmc/Quantifiers-if/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
Expand Down
10 changes: 5 additions & 5 deletions regression/cbmc/Quantifiers-initialisation/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
Expand Down
10 changes: 5 additions & 5 deletions regression/cbmc/Quantifiers-initialisation2/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
Expand Down
12 changes: 6 additions & 6 deletions regression/cbmc/Quantifiers-not-exists/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
Expand Down
10 changes: 5 additions & 5 deletions regression/cbmc/Quantifiers-not/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
Expand Down
10 changes: 5 additions & 5 deletions regression/cbmc/Quantifiers-two-dimension-array/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
Expand Down
4 changes: 2 additions & 2 deletions regression/cbmc/Quantifiers-type/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/Undefined_Shift1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
--
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/fgets1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 2 additions & 2 deletions regression/cbmc/gcc_bswap1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 1 addition & 1 deletion regression/cbmc/goto4/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 1 addition & 1 deletion regression/cbmc/memcpy1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 4 additions & 4 deletions regression/cbmc/memory_allocation1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 1 addition & 1 deletion regression/cbmc/memset1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 1 addition & 1 deletion regression/cbmc/memset3/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 1 addition & 1 deletion regression/cbmc/pipe1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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 changes: 28 additions & 28 deletions regression/cbmc/pointer-extra-checks/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Loading