diff --git a/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.desc b/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.desc index 17c107b17d3..031085bf6ed 100644 --- a/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.desc +++ b/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.desc @@ -1,6 +1,6 @@ CORE pointer_subtraction.c ---no-signed-overflow-check --trace +--no-signed-overflow-check --trace --no-pointer-check \[main\.assertion\.1\] line \d+ expected failure after pointer manipulation: FAILURE \[main\.assertion\.2\] line \d+ expected successful after pointer manipulation: SUCCESS \[main\.assertion\.3\] line \d+ expected failure after pointer manipulation: FAILURE diff --git a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc index c66861d774a..c1bdadc66eb 100644 --- a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc +++ b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc @@ -1,6 +1,6 @@ CORE pointers_assume.c ---trace +--trace --no-pointer-check \[main\.assertion\.1\] line \d+ x == y: expected failure: FAILURE \[main\.assertion\.2\] line \d+ z >= x: expected successful: SUCCESS \[main\.assertion\.3\] line \d+ z <= y: expected successful: SUCCESS diff --git a/regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc b/regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc index f938a299f5b..70c5dc016ad 100644 --- a/regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc +++ b/regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc @@ -4,7 +4,7 @@ invalid_index_range.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -\[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 20\) && a\[i\] == i \*i \}: SUCCESS +^\[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 20\) && a\[i\] == i \*i \}: UNKNOWN$ line 9 dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE -- -- diff --git a/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc b/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc index a2ee20ffd2d..6066f2b9402 100644 --- a/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc +++ b/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc @@ -4,8 +4,8 @@ smt_missing_range_check.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -\[main\.assertion\.1\] line \d assertion __CPROVER_exists \{ int i; a\[i\] == i \*i \}: SUCCESS -\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE +^\[main\.assertion\.1\] line \d assertion __CPROVER_exists \{ int i; a\[i\] == i \*i \}: UNKNOWN$ +^\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE$ -- -- Check that memory checks fail for pointer dereferences inside an existential diff --git a/regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc b/regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc index bbc8bd2271b..2619d90fe09 100644 --- a/regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc +++ b/regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc @@ -3,13 +3,13 @@ test_malloc_less_than_bound.c --no-malloc-may-fail --pointer-check ^EXIT=10$ ^SIGNAL=0$ -\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS -\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS -\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS -\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS -\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS -\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE -\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: SUCCESS +^\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: UNKNOWN$ +^\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$ +^\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$ +^\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$ +^\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$ +^\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE$ +^\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: UNKNOWN$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/cbmc/Function_Pointer18/test.desc b/regression/cbmc/Function_Pointer18/test.desc index 7aacf515906..8e35981a225 100644 --- a/regression/cbmc/Function_Pointer18/test.desc +++ b/regression/cbmc/Function_Pointer18/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-pointer-check ^EXIT=10$ ^SIGNAL=0$ \[f2.assertion.1\] line [0-9]+ assertion 0: SUCCESS diff --git a/regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc b/regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc index b0e774c5ed5..029b2c6b908 100644 --- a/regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc +++ b/regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc @@ -1,6 +1,6 @@ CORE main.c ---function foo +--function foo --no-pointer-check ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 5: FAILURE$ ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 4: SUCCESS$ ^EXIT=10$ diff --git a/regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc b/regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc index 8becf23aa28..0b7199d2af1 100644 --- a/regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc +++ b/regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc @@ -1,6 +1,6 @@ CORE main.c ---function foo +--function foo --no-pointer-check ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 5: FAILURE$ ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) >= 4: SUCCESS$ ^EXIT=10$ diff --git a/regression/cbmc/array-cell-sensitivity10/test_execution.desc b/regression/cbmc/array-cell-sensitivity10/test_execution.desc index 1e8aa561e48..e206cd6f5d3 100644 --- a/regression/cbmc/array-cell-sensitivity10/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity10/test_execution.desc @@ -1,6 +1,6 @@ CORE test.c - +--no-pointer-check ^VERIFICATION FAILED$ ^\[main.assertion\.1\] line 16.*SUCCESS$ ^\[main.assertion\.2\] line 17.*FAILURE$ diff --git a/regression/cbmc/array-cell-sensitivity3/test_execution.desc b/regression/cbmc/array-cell-sensitivity3/test_execution.desc index 52bf413ffd9..94e805c288a 100644 --- a/regression/cbmc/array-cell-sensitivity3/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity3/test_execution.desc @@ -1,6 +1,6 @@ CORE test.c - +--no-pointer-check ^VERIFICATION FAILED$ ^\[main.assertion\.1\] line 9.*SUCCESS$ ^\[main.assertion\.2\] line 10.*FAILURE$ diff --git a/regression/cbmc/array-cell-sensitivity7/test_execution.desc b/regression/cbmc/array-cell-sensitivity7/test_execution.desc index 4e577438df9..fef0c9858b5 100644 --- a/regression/cbmc/array-cell-sensitivity7/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity7/test_execution.desc @@ -1,6 +1,6 @@ CORE test.c - +--no-pointer-check ^VERIFICATION FAILED$ ^\[main.assertion\.1\] line 10.*SUCCESS$ ^\[main.assertion\.2\] line 11.*FAILURE$ diff --git a/regression/cbmc/array-cell-sensitivity8/test_execution.desc b/regression/cbmc/array-cell-sensitivity8/test_execution.desc index 6cbd3a308e8..7c4e27f11b5 100644 --- a/regression/cbmc/array-cell-sensitivity8/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity8/test_execution.desc @@ -1,6 +1,6 @@ CORE test.c - +--no-pointer-check ^VERIFICATION FAILED$ ^\[main.assertion\.1\] line 11.*SUCCESS$ ^\[main.assertion\.2\] line 12.*FAILURE$ diff --git a/regression/cbmc/byte_update14/test.desc b/regression/cbmc/byte_update14/test.desc index 99e319ce543..3e8b2aa288e 100644 --- a/regression/cbmc/byte_update14/test.desc +++ b/regression/cbmc/byte_update14/test.desc @@ -1,6 +1,6 @@ CORE test.c - +--no-pointer-check ^VERIFICATION FAILED$ ^\[main.assertion\.1\] line 10.*SUCCESS$ ^\[main.assertion\.2\] line 11.*FAILURE$ diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc index b475124244b..ffa7f87988a 100644 --- a/regression/cbmc/memory_allocation1/test.desc +++ b/regression/cbmc/memory_allocation1/test.desc @@ -6,7 +6,7 @@ main.c ^\[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\.assertion\.2\] .* assertion \*\(p\+1\)==42: UNKNOWN$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/pointer-extra-checks/test.desc b/regression/cbmc/pointer-extra-checks/test.desc index 03bece93ba2..9516ae2e9af 100644 --- a/regression/cbmc/pointer-extra-checks/test.desc +++ b/regression/cbmc/pointer-extra-checks/test.desc @@ -4,10 +4,10 @@ main.c ^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.2\] .* dereference failure: dead object in \*q: UNKNOWN$ +^\[main.pointer_dereference.3\] .* dereference failure: pointer outside object bounds in \*q: UNKNOWN$ +^\[main.pointer_dereference.4\] .* dereference failure: deallocated dynamic object in \*r: UNKNOWN$ +^\[main.pointer_dereference.5\] .* dereference failure: pointer outside dynamic object bounds in \*r: UNKNOWN$ ^\[main.pointer_dereference.6\] .* dereference failure: pointer NULL in \*s: FAILURE$ ^\[main.pointer_dereference.7\] .* dereference failure: pointer invalid in \*s: FAILURE$ ^\[main.pointer_dereference.8\] .* dereference failure: deallocated dynamic object in \*s: FAILURE$ diff --git a/regression/cbmc/ptr_arithmetic_on_null/test.desc b/regression/cbmc/ptr_arithmetic_on_null/test.desc index b7c0190dbc5..877360e6196 100644 --- a/regression/cbmc/ptr_arithmetic_on_null/test.desc +++ b/regression/cbmc/ptr_arithmetic_on_null/test.desc @@ -4,9 +4,9 @@ main.c ^\[main.assertion.1\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ (\(.*\))?1: SUCCESS$ ^\[main.assertion.2\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 - (\(.*\))?1: SUCCESS$ ^\[main.assertion.3\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ \(.*\)offset: SUCCESS$ -^\[main.assertion.4\] line .* assertion \(char \*\)\(void \*\)0 - \(char \*\)\(void \*\)0 == (\(.*\))?0: SUCCESS$ +^\[main.assertion.4\] line .* assertion \(char \*\)\(void \*\)0 - \(char \*\)\(void \*\)0 == (\(.*\))?0: UNKNOWN$ ^\[main.assertion.5\] line .* assertion ptr - \(signed int \*\)\(void \*\)0 == (\(.*\))?0: FAILURE$ -^\[main.assertion.6\] line .* assertion \(ptr - (\(.*\))?1\) \+ (\(.*\))?1 == \(\(.* \*\)NULL\): SUCCESS$ +^\[main.assertion.6\] line .* assertion \(ptr - (\(.*\))?1\) \+ (\(.*\))?1 == \(\(.* \*\)NULL\): UNKNOWN$ ^\[main.assertion.7\] line .* assertion \(ptr - (\(.*\))?1\) \+ (\(.*\))?1 == \(\(.* \*\)NULL\): FAILURE$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/switch8/test.desc b/regression/cbmc/switch8/test.desc index f054d2889bc..01f98130229 100644 --- a/regression/cbmc/switch8/test.desc +++ b/regression/cbmc/switch8/test.desc @@ -8,7 +8,7 @@ main.c ^\[main\.pointer_dereference\.1\] line 36 dereference failure: dead object in \*p: SUCCESS$ ^\[main\.pointer_dereference\.2\] line 36 dereference failure: pointer outside object bounds in \*p: SUCCESS$ ^\[main\.assertion\.3\] line 42 assertion \*p == 42: FAILURE$ -^\[main\.pointer_dereference\.5\] line 42 dereference failure: pointer outside object bounds in \*p: SUCCESS$ +^\[main\.pointer_dereference\.5\] line 42 dereference failure: pointer outside object bounds in \*p: UNKNOWN$ ^\[main\.pointer_dereference\.3\] line 42 dereference failure: pointer NULL in \*p: SUCCESS$ ^\[main\.pointer_dereference\.4\] line 42 dereference failure: dead object in \*p: FAILURE$ ^\[main\.assertion\.4\] line 49 assertion e == 42: FAILURE$ diff --git a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc index 779e626fd9b..a74caa5b7f2 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[f2.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: FAILURE$ -^\[f2.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ +^\[f2.assigns.\d+\] line \d+ Check that p->size is assignable: UNKNOWN$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_replace_conditional_targets/main.c b/regression/contracts-dfcc/assigns_replace_conditional_targets/main.c index 7226f2250f2..10956ed0194 100644 --- a/regression/contracts-dfcc/assigns_replace_conditional_targets/main.c +++ b/regression/contracts-dfcc/assigns_replace_conditional_targets/main.c @@ -1,4 +1,5 @@ #include +#include bool nz(int x) { @@ -46,6 +47,9 @@ int main() old_y = y; char *z = malloc(1); + if(z == NULL) + return; + *z = '0'; foo(a, &x, &y, z); diff --git a/regression/contracts-dfcc/assigns_replace_conditional_targets/test.desc b/regression/contracts-dfcc/assigns_replace_conditional_targets/test.desc index 99921e61ebd..5692335e532 100644 --- a/regression/contracts-dfcc/assigns_replace_conditional_targets/test.desc +++ b/regression/contracts-dfcc/assigns_replace_conditional_targets/test.desc @@ -2,13 +2,13 @@ CORE main.c --dfcc main --replace-call-with-contract foo ^main.c function main$ -^\[main\.assertion\.\d+\] line 55 a unchanged, expecting SUCCESS: SUCCESS$ -^\[main\.assertion\.\d+\] line 57 x changed, expecting FAILURE: FAILURE$ -^\[main\.assertion\.\d+\] line 59 x unchanged, expecting SUCCESS: SUCCESS$ -^\[main\.assertion\.\d+\] line 62 y changed, expecting FAILURE: FAILURE$ -^\[main\.assertion\.\d+\] line 64 y unchanged, expecting SUCCESS: SUCCESS$ -^\[main\.assertion\.\d+\] line 67 z changed, expecting FAILURE: FAILURE$ -^\[main\.assertion\.\d+\] line 69 z unchanged, expecting SUCCESS: SUCCESS$ +^\[main\.assertion\.\d+\] line 59 a unchanged, expecting SUCCESS: SUCCESS$ +^\[main\.assertion\.\d+\] line 61 x changed, expecting FAILURE: FAILURE$ +^\[main\.assertion\.\d+\] line 63 x unchanged, expecting SUCCESS: SUCCESS$ +^\[main\.assertion\.\d+\] line 66 y changed, expecting FAILURE: FAILURE$ +^\[main\.assertion\.\d+\] line 68 y unchanged, expecting SUCCESS: SUCCESS$ +^\[main\.assertion\.\d+\] line 71 z changed, expecting FAILURE: FAILURE$ +^\[main\.assertion\.\d+\] line 73 z unchanged, expecting SUCCESS: SUCCESS$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/invar_dynamic_struct_member/main.c b/regression/contracts-dfcc/invar_dynamic_struct_member/main.c index 71af535f801..f35aaabc136 100644 --- a/regression/contracts-dfcc/invar_dynamic_struct_member/main.c +++ b/regression/contracts-dfcc/invar_dynamic_struct_member/main.c @@ -1,3 +1,5 @@ +#include + typedef struct test { int x; @@ -6,6 +8,8 @@ typedef struct test void main() { struct test *t = malloc(sizeof(test)); + if(t == NULL) + return; t->x = 0; unsigned n; diff --git a/regression/contracts-dfcc/invar_dynamic_struct_member/test.desc b/regression/contracts-dfcc/invar_dynamic_struct_member/test.desc index 5346bc358b7..7ab31ab5ce8 100644 --- a/regression/contracts-dfcc/invar_dynamic_struct_member/test.desc +++ b/regression/contracts-dfcc/invar_dynamic_struct_member/test.desc @@ -3,14 +3,14 @@ main.c --dfcc main --apply-loop-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main.loop_assigns.\d+\] line 12 Check assigns clause inclusion for loop .*: SUCCESS$ -^\[main.loop_invariant_base.\d+\] line 12 Check invariant before entry for loop .*: SUCCESS$ -^\[main.loop_invariant_step.\d+\] line 12 Check invariant after step for loop .*: SUCCESS$ -^\[main.loop_step_unwinding.\d+\] line 12 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+\] line 16 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 16 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 16 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 16 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] line 22 Check that t->x is assignable: SUCCESS$ -^\[main.assigns.\d+\] line 25 Check that t->x is assignable: SUCCESS$ -^\[main.assertion.\d+\] line 29 assertion .*: FAILURE$ +^\[main.assigns.\d+\] line 26 Check that t->x is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 29 Check that t->x is assignable: SUCCESS$ +^\[main.assertion.\d+\] line 33 assertion .*: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/loop_assigns-02/main.c b/regression/contracts-dfcc/loop_assigns-02/main.c index d4b45140be3..f07321e6852 100644 --- a/regression/contracts-dfcc/loop_assigns-02/main.c +++ b/regression/contracts-dfcc/loop_assigns-02/main.c @@ -11,7 +11,11 @@ struct blob void main() { struct blob *b = malloc(sizeof(struct blob)); + if(b == NULL) + return; b->data = malloc(SIZE); + if(b->data == NULL) + return; b->data[5] = 0; for(unsigned i = 0; i < SIZE; i++) diff --git a/regression/contracts-dfcc/loop_assigns-02/test.desc b/regression/contracts-dfcc/loop_assigns-02/test.desc index 100dfcb2dc7..3548639247f 100644 --- a/regression/contracts-dfcc/loop_assigns-02/test.desc +++ b/regression/contracts-dfcc/loop_assigns-02/test.desc @@ -3,10 +3,10 @@ main.c --dfcc main --apply-loop-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main.loop_assigns.\d+\] line 17 Check assigns clause inclusion for loop .*: SUCCESS$ -^\[main.loop_invariant_base.\d+\] line 17 Check invariant before entry for loop .*: SUCCESS$ -^\[main.loop_invariant_step.\d+\] line 17 Check invariant after step for loop .*: SUCCESS$ -^\[main.loop_step_unwinding.\d+\] line 17 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+\] line 21 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 21 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 21 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 21 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ ^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/loop_assigns-04/main.c b/regression/contracts-dfcc/loop_assigns-04/main.c index 255d7aed40e..1f7a6882dc6 100644 --- a/regression/contracts-dfcc/loop_assigns-04/main.c +++ b/regression/contracts-dfcc/loop_assigns-04/main.c @@ -12,7 +12,11 @@ void main() { int y; struct blob *b = malloc(sizeof(struct blob)); + if(b == NULL) + return; b->data = malloc(SIZE); + if(b->data == NULL) + return; b->data[5] = 0; for(unsigned i = 0; i < SIZE; i++) diff --git a/regression/contracts-dfcc/loop_assigns-04/test.desc b/regression/contracts-dfcc/loop_assigns-04/test.desc index 4c171095b11..bb9a49b8307 100644 --- a/regression/contracts-dfcc/loop_assigns-04/test.desc +++ b/regression/contracts-dfcc/loop_assigns-04/test.desc @@ -3,14 +3,14 @@ main.c --dfcc main --apply-loop-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main.loop_assigns.\d+\] line 18 Check assigns clause inclusion for loop .*: SUCCESS$ -^\[main.loop_invariant_base.\d+\] line 18 Check invariant before entry for loop .*: SUCCESS$ -^\[main.loop_invariant_step.\d+\] line 18 Check invariant after step for loop .*: SUCCESS$ -^\[main.loop_step_unwinding.\d+\] line 18 Check step was unwound for loop .*: SUCCESS$ -^\[main.loop_assigns.\d+\] line 27 Check assigns clause inclusion for loop .*: FAILURE$ -^\[main.loop_invariant_base.\d+\] line 27 Check invariant before entry for loop .*: SUCCESS$ -^\[main.loop_invariant_step.\d+\] line 27 Check invariant after step for loop .*: SUCCESS$ -^\[main.loop_step_unwinding.\d+\] line 27 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+\] line 22 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 22 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 22 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 22 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+\] line 31 Check assigns clause inclusion for loop .*: FAILURE$ +^\[main.loop_invariant_base.\d+\] line 31 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 31 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 31 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ ^\[main.assigns.\d+\] .* Check that j is assignable: SUCCESS$ ^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc index 3bc041ab15c..d91072b7143 100644 --- a/regression/contracts/assigns_enforce_free_dead/test.desc +++ b/regression/contracts/assigns_enforce_free_dead/test.desc @@ -7,10 +7,10 @@ main.c ^\[foo.assigns.\d+\] line 7 Check that \*\(\*p\) is assignable: SUCCESS$ ^\[foo.assigns.\d+\] line 24 Check that \*\(\*p\) is assignable: FAILURE$ ^\[foo.assigns.\d+\] line \d+ Check that \*p is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*q is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*w is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*q is assignable: UNKNOWN$ +^\[foo.assigns.\d+\] line \d+ Check that \*w is assignable: UNKNOWN$ +^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: UNKNOWN$ +^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)z\) is assignable: UNKNOWN$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_dynamic_struct_member/test.desc b/regression/contracts/invar_dynamic_struct_member/test.desc index d6653a12b0c..15278491b24 100644 --- a/regression/contracts/invar_dynamic_struct_member/test.desc +++ b/regression/contracts/invar_dynamic_struct_member/test.desc @@ -3,11 +3,11 @@ main.c --apply-loop-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ -^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] line 22 Check that t->x is assignable: SUCCESS$ -^\[main.assigns.\d+\] line 25 Check that t->x is assignable: SUCCESS$ +^\[main\.\d+\] .* Check loop invariant before entry: UNKNOWN$ +^\[main\.\d+\] .* Check that loop invariant is preserved: UNKNOWN$ +^\[main.assigns.\d+\] .* Check that i is assignable: UNKNOWN$ +^\[main.assigns.\d+\] line 22 Check that t->x is assignable: UNKNOWN$ +^\[main.assigns.\d+\] line 25 Check that t->x is assignable: UNKNOWN$ ^\[main.assertion.1\] .* assertion .*: FAILURE$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/loop_assigns-02/test.desc b/regression/contracts/loop_assigns-02/test.desc index 205356864ef..2c3eb25c624 100644 --- a/regression/contracts/loop_assigns-02/test.desc +++ b/regression/contracts/loop_assigns-02/test.desc @@ -3,10 +3,10 @@ main.c --apply-loop-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ -^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.\d+\] .* Check loop invariant before entry: UNKNOWN$ +^\[main.assigns.\d+\] .* Check that i is assignable: UNKNOWN$ ^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$ -^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: UNKNOWN$ ^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/loop_assigns-04/test.desc b/regression/contracts/loop_assigns-04/test.desc index 95d9f0f9d79..8cd0eb461da 100644 --- a/regression/contracts/loop_assigns-04/test.desc +++ b/regression/contracts/loop_assigns-04/test.desc @@ -3,9 +3,9 @@ main.c --apply-loop-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that j is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: UNKNOWN$ +^\[main.assigns.\d+\] .* Check that j is assignable: UNKNOWN$ +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: UNKNOWN$ ^\[main.assigns.\d+\] .* Check that y is assignable: FAILURE$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/loop_assigns-fail/test.desc b/regression/contracts/loop_assigns-fail/test.desc index 38480d617d7..95900c6ea1b 100644 --- a/regression/contracts/loop_assigns-fail/test.desc +++ b/regression/contracts/loop_assigns-fail/test.desc @@ -3,7 +3,7 @@ main.c --apply-loop-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: UNKNOWN$ ^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$ ^VERIFICATION FAILED$ -- 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 24289e470a2..580857e32b4 100644 --- a/regression/goto-instrument/generate-function-body-complex-struct/test.desc +++ b/regression/goto-instrument/generate-function-body-complex-struct/test.desc @@ -9,9 +9,9 @@ main.c \[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.7\] .* assertion main_struct.struct_contents.some_constant == 20: UNKNOWN \[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.9\] .* assertion child_struct.struct_contents.some_variable == 11: UNKNOWN +\[main.assertion.10\] .* assertion child_struct.union_contents.some_integer == 31: UNKNOWN +\[main.assertion.11\] .* assertion !child_struct.pointer_contents: UNKNOWN ^VERIFICATION FAILED$ diff --git a/regression/goto-instrument/nondet_static_exclude/test.desc b/regression/goto-instrument/nondet_static_exclude/test.desc index 5afec178253..2e7df08b39e 100644 --- a/regression/goto-instrument/nondet_static_exclude/test.desc +++ b/regression/goto-instrument/nondet_static_exclude/test.desc @@ -13,6 +13,6 @@ assertion test4->b == 4: SUCCESS assertion test5->a == 5: FAILURE assertion test5->b == 2: FAILURE assertion value == 7: FAILURE -assertion value == 5: SUCCESS +assertion value == 5: UNKNOWN -- -- diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp index 4f3f2499919..f829ebeda7e 100644 --- a/src/ansi-c/goto-conversion/goto_check_c.cpp +++ b/src/ansi-c/goto-conversion/goto_check_c.cpp @@ -1368,7 +1368,7 @@ void goto_check_ct::pointer_rel_check( c.assertion, "pointer relation: " + c.description, "pointer arithmetic", - false, // fatal + true, // fatal expr.find_source_location(), pointer, guard); @@ -1427,7 +1427,7 @@ void goto_check_ct::pointer_overflow_check( c.assertion, "pointer arithmetic: " + c.description, "pointer arithmetic", - false, // fatal + true, // fatal expr.find_source_location(), expr, guard); @@ -1469,7 +1469,7 @@ void goto_check_ct::pointer_validity_check( c.assertion, "dereference failure: " + c.description, "pointer dereference", - false, // fatal + true, // fatal src_expr.find_source_location(), src_expr, guard);