diff --git a/regression/contracts/assigns_enforce_17/test.desc b/regression/contracts/assigns_enforce_17/test.desc index 7fd17053d79..03f5e53fb38 100644 --- a/regression/contracts/assigns_enforce_17/test.desc +++ b/regression/contracts/assigns_enforce_17/test.desc @@ -3,7 +3,7 @@ main.c --enforce-all-contracts ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.\d+\] line \d+ assertion x \=\= 0\: SUCCESS$ +^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_04/test.desc b/regression/contracts/assigns_enforce_structs_04/test.desc index cac8400fdf6..98d5e666406 100644 --- a/regression/contracts/assigns_enforce_structs_04/test.desc +++ b/regression/contracts/assigns_enforce_structs_04/test.desc @@ -3,10 +3,10 @@ main.c --enforce-all-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[f1.\d+\] line \d+ Check that p\-\>y is assignable\: FAILURE$ -^\[f2.\d+\] line \d+ Check that p\-\>x is assignable\: FAILURE$ -^\[f3.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$ -^\[f4.\d+\] line \d+ Check that p is assignable\: FAILURE$ +^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$ +^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$ +^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ +^\[f4.\d+\] line \d+ Check that p is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_05/test.desc b/regression/contracts/assigns_enforce_structs_05/test.desc index 239a259798c..160d5b67bea 100644 --- a/regression/contracts/assigns_enforce_structs_05/test.desc +++ b/regression/contracts/assigns_enforce_structs_05/test.desc @@ -3,10 +3,10 @@ main.c --enforce-all-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[f1.\d+\] line \d+ Check that p\-\>y is assignable\: FAILURE$ -^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)0\] is assignable\: SUCCESS$ -^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)1\] is assignable\: SUCCESS$ -^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)2\] is assignable\: SUCCESS$ +^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$ +^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)0\] is assignable: SUCCESS$ +^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)1\] is assignable: SUCCESS$ +^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)2\] is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_06/test.desc b/regression/contracts/assigns_enforce_structs_06/test.desc index 69f67cdede5..b3d52815f80 100644 --- a/regression/contracts/assigns_enforce_structs_06/test.desc +++ b/regression/contracts/assigns_enforce_structs_06/test.desc @@ -3,14 +3,14 @@ main.c --enforce-all-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: SUCCESS$ -^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)1\] is assignable\: SUCCESS$ -^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)2\] is assignable\: SUCCESS$ -^\[f1.\d+\] line \d+ Check that p\-\>size is assignable\: FAILURE$ -^\[f2.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: FAILURE$ -^\[f2.\d+\] line \d+ Check that p\-\>size is assignable\: SUCCESS$ -^\[f3.\d+\] line \d+ Check that p\-\>buf is assignable\: SUCCESS$ -^\[f3.\d+\] line \d+ Check that p\-\>size is assignable\: SUCCESS$ +^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)1\] is assignable: SUCCESS$ +^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)2\] is assignable: SUCCESS$ +^\[f1.\d+\] line \d+ Check that p->size is assignable: FAILURE$ +^\[f2.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f2.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ +^\[f3.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$ +^\[f3.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_07/main.c b/regression/contracts/assigns_enforce_structs_07/main.c new file mode 100644 index 00000000000..4651df53afa --- /dev/null +++ b/regression/contracts/assigns_enforce_structs_07/main.c @@ -0,0 +1,34 @@ +#include +#include +#include + +struct pair +{ + uint8_t *buf; + size_t size; +}; + +struct pair_of_pairs +{ + struct pair *p; +}; + +void f1(struct pair *p) __CPROVER_assigns(*(p->buf)) +{ + p->buf[0] = 0; +} + +void f2(struct pair_of_pairs *pp) __CPROVER_assigns(*(pp->p->buf)) +{ + pp->p->buf[0] = 0; +} + +int main() +{ + struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL; + f1(p); + struct pair_of_pairs *pp = malloc(sizeof(*pp)); + f2(pp); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_structs_07/test.desc b/regression/contracts/assigns_enforce_structs_07/test.desc new file mode 100644 index 00000000000..6e2f848eb94 --- /dev/null +++ b/regression/contracts/assigns_enforce_structs_07/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts _ --pointer-check +^EXIT=10$ +^SIGNAL=0$ +^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in p->buf: FAILURE$ +^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in pp->p->buf: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Checks whether CBMC properly evaluates write set of members +from invalid objects. In this case, they are not writable. diff --git a/regression/contracts/assigns_replace_07/main.c b/regression/contracts/assigns_replace_07/main.c new file mode 100644 index 00000000000..16bf52c0ab8 --- /dev/null +++ b/regression/contracts/assigns_replace_07/main.c @@ -0,0 +1,25 @@ +#include +#include +#include + +struct pair +{ + uint8_t *buf; + size_t size; +}; + +void f1(struct pair *p) __CPROVER_assigns(*(p->buf)) + __CPROVER_ensures(p->buf[0] == 0) +{ + p->buf[0] = 0; +} + +int main() +{ + struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL; + f1(p); + // clang-format off + assert(p != NULL ==> p->buf[0] == 0); + // clang-format on + return 0; +} diff --git a/regression/contracts/assigns_replace_07/test.desc b/regression/contracts/assigns_replace_07/test.desc new file mode 100644 index 00000000000..d7c4d1a0492 --- /dev/null +++ b/regression/contracts/assigns_replace_07/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--replace-all-calls-with-contracts _ --pointer-check +^EXIT=10$ +^SIGNAL=0$ +^\[pointer\_dereference.\d+\] file main.c line \d+ dereference failure: pointer NULL in p->buf: FAILURE$ +^\[main.assertion.\d+\] line \d+ assertion p \!\= NULL \=\=> p->buf\[0\] \=\= 0: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Checks whether CBMC properly evaluates write set of members +from invalid objects. In this case, they are not writable. diff --git a/regression/contracts/assigns_type_checking_valid_cases/test.desc b/regression/contracts/assigns_type_checking_valid_cases/test.desc index 9db0bb7057b..0793735943f 100644 --- a/regression/contracts/assigns_type_checking_valid_cases/test.desc +++ b/regression/contracts/assigns_type_checking_valid_cases/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[foo1.\d+\] line \d+ Check that a is assignable: SUCCESS$ -^\[foo10.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$ -^\[foo10.\d+\] line \d+ Check that buffer\-\>aux\.allocated is assignable: SUCCESS$ +^\[foo10.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ +^\[foo10.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$ ^\[foo2.\d+\] line \d+ Check that b is assignable: SUCCESS$ ^\[foo3.\d+\] line \d+ Check that b is assignable: SUCCESS$ ^\[foo3.\d+\] line \d+ Check that y is assignable: SUCCESS$ @@ -14,10 +14,10 @@ main.c ^\[foo4.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^\[foo5.\d+\] line \d+ Check that buffer.data is assignable: SUCCESS$ ^\[foo5.\d+\] line \d+ Check that buffer.len is assignable: SUCCESS$ -^\[foo6.\d+\] line \d+ Check that \*buffer\-\>data is assignable: SUCCESS$ -^\[foo6.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$ -^\[foo7.\d+\] line \d+ Check that \*buffer\-\>data is assignable: SUCCESS$ -^\[foo7.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$ +^\[foo6.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ +^\[foo6.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ +^\[foo7.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ +^\[foo7.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$ ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$ ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$ diff --git a/regression/contracts/assigns_validity_pointer_01/test.desc b/regression/contracts/assigns_validity_pointer_01/test.desc index 9ef4d9894d7..149013fd7a7 100644 --- a/regression/contracts/assigns_validity_pointer_01/test.desc +++ b/regression/contracts/assigns_validity_pointer_01/test.desc @@ -16,9 +16,6 @@ ASSUME .*::tmp_if_expr\$\d IF ¬\(z ≠ NULL\) THEN GOTO \d ASSIGN .*::tmp_if_expr\$\d := \(\*z = 7 \? true : false\) ASSUME .*::tmp_if_expr\$\d -// foo -ASSUME \*.*::tmp_cc\$\d > 0 -ASSERT \*.*::tmp_cc\$\d = 3 -- \[3\] file main\.c line 6 assertion: FAILURE -- diff --git a/regression/contracts/assigns_validity_pointer_02/test.desc b/regression/contracts/assigns_validity_pointer_02/test.desc index ebfee6dc26a..f8579bd42ba 100644 --- a/regression/contracts/assigns_validity_pointer_02/test.desc +++ b/regression/contracts/assigns_validity_pointer_02/test.desc @@ -5,9 +5,6 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ //^([foo\.1] line 15 assertion: FAILURE) -// foo -ASSUME \*.*::tmp_cc\$\d > 0 -ASSERT \*.*::tmp_cc\$\d = 3 -- \[foo\.1\] line 24 assertion: FAILURE \[foo\.3\] line 27 assertion: FAILURE diff --git a/regression/contracts/assigns_validity_pointer_03/test.desc b/regression/contracts/assigns_validity_pointer_03/test.desc index 7c04f9cff70..a444bb19dce 100644 --- a/regression/contracts/assigns_validity_pointer_03/test.desc +++ b/regression/contracts/assigns_validity_pointer_03/test.desc @@ -7,7 +7,7 @@ main.c // bar ASSERT \*x > 0 IF !\(\*x == 3\) THEN GOTO \d -tmp_if_expr = \*y == 5 \? true \: false; +tmp_if_expr = \*y == 5 \? true : false; ASSUME tmp_if_expr // baz ASSUME \*z == 7 diff --git a/regression/contracts/assigns_validity_pointer_04/test.desc b/regression/contracts/assigns_validity_pointer_04/test.desc index 11aec0dea4b..98d5c698b9f 100644 --- a/regression/contracts/assigns_validity_pointer_04/test.desc +++ b/regression/contracts/assigns_validity_pointer_04/test.desc @@ -11,9 +11,6 @@ ASSIGN goto_convertt::tmp_if_expr := \(\*foo::1::y = 5 \? true : false\) ASSUME .*::tmp_if_expr // baz ASSUME \*z = 7 -// foo -ASSUME \*.*::tmp_cc\$\d > 0 -ASSERT \*.*::tmp_cc\$\d = 3 -- -- Verification: diff --git a/regression/contracts/history-pointer-enforce-01/test.desc b/regression/contracts/history-pointer-enforce-01/test.desc index 594cb8af05d..650511f99ad 100644 --- a/regression/contracts/history-pointer-enforce-01/test.desc +++ b/regression/contracts/history-pointer-enforce-01/test.desc @@ -4,7 +4,6 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -ASSERT \*.*::tmp_cc\$\d = .*::tmp_cc\$\d \+ 5 -- -- Verification: diff --git a/regression/contracts/history-pointer-enforce-02/test.desc b/regression/contracts/history-pointer-enforce-02/test.desc index bd08337d8ee..009bf0343f7 100644 --- a/regression/contracts/history-pointer-enforce-02/test.desc +++ b/regression/contracts/history-pointer-enforce-02/test.desc @@ -4,7 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -ASSERT \*.*::tmp_cc\$\d < .*::tmp_cc\$\d \+ 5 -- -- Verification: diff --git a/regression/contracts/history-pointer-enforce-08/test.desc b/regression/contracts/history-pointer-enforce-08/test.desc index 9049c0bc86c..bb5a41b2f2f 100644 --- a/regression/contracts/history-pointer-enforce-08/test.desc +++ b/regression/contracts/history-pointer-enforce-08/test.desc @@ -4,7 +4,6 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -ASSERT \*\(.*::tmp_cc\$\d\.y\) = .*::tmp_cc\$\d \+ 5 -- -- Verification: diff --git a/regression/contracts/history-pointer-enforce-09/test.desc b/regression/contracts/history-pointer-enforce-09/test.desc index 59434031a4b..14a9fc77b75 100644 --- a/regression/contracts/history-pointer-enforce-09/test.desc +++ b/regression/contracts/history-pointer-enforce-09/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ -^\[foo.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$ +^\[foo.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/history-pointer-enforce-10/test.desc b/regression/contracts/history-pointer-enforce-10/test.desc index 46efe6b2767..f333b70337d 100644 --- a/regression/contracts/history-pointer-enforce-10/test.desc +++ b/regression/contracts/history-pointer-enforce-10/test.desc @@ -3,16 +3,16 @@ main.c --enforce-all-contracts ^EXIT=0$ ^SIGNAL=0$ -^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$ -^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$ -^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$ -^\[bar.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$ -^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$ -^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*p\-\>y is assignable\: SUCCESS$ -^\[foo.\d+\] line \d+ Check that z is assignable\: SUCCESS$ -^\[main.assertion.\d+\] line \d+ assertion \*\(p\-\>y\) == 7\: SUCCESS$ -^\[main.assertion.\d+\] line \d+ assertion \*\(p\-\>y\) == -1\: SUCCESS$ +^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ +^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ +^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$ +^\[bar.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ +^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$ +^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ +^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == 7: SUCCESS$ +^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == -1: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/history-pointer-enforce-11/test.desc b/regression/contracts/history-pointer-enforce-11/test.desc index 8359fef2840..38a8cb3c313 100644 --- a/regression/contracts/history-pointer-enforce-11/test.desc +++ b/regression/contracts/history-pointer-enforce-11/test.desc @@ -3,8 +3,8 @@ main.c --enforce-all-contracts ^EXIT=0$ ^SIGNAL=0$ -^\[postcondition.\d+\] Check ensures clause\: SUCCESS$ -^\[foo.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$ +^\[postcondition.\d+\] Check ensures clause: SUCCESS$ +^\[foo.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/history-pointer-replace-04/test.desc b/regression/contracts/history-pointer-replace-04/test.desc index 7b40a853944..633eb5b9a04 100644 --- a/regression/contracts/history-pointer-replace-04/test.desc +++ b/regression/contracts/history-pointer-replace-04/test.desc @@ -3,8 +3,8 @@ main.c --replace-all-calls-with-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[precondition.\d+\] file main.c line \d+ Check requires clause\: SUCCESS$ -^\[main.assertion.\d+\] line \d+ assertion p\-\>y \!\= 7\: FAILURE$ +^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$ +^\[main.assertion.\d+\] line \d+ assertion p->y \!\= 7: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/test_array_memory_replace/test.desc b/regression/contracts/test_array_memory_replace/test.desc index 5c5b0494a33..977e047d497 100644 --- a/regression/contracts/test_array_memory_replace/test.desc +++ b/regression/contracts/test_array_memory_replace/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS -\[main.assertion.\d+\] line \d+ assertion o \>\= 10 \&\& o \=\= \*n \+ 5: SUCCESS +\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS \[main.assertion.\d+\] line \d+ assertion n\[9\] == 113: SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/test_array_memory_too_small_replace/test.desc b/regression/contracts/test_array_memory_too_small_replace/test.desc index 9d20386dcca..d073a47a947 100644 --- a/regression/contracts/test_array_memory_too_small_replace/test.desc +++ b/regression/contracts/test_array_memory_too_small_replace/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ \[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE -\[main.assertion.\d+\] line \d+ assertion o \>\= 10 \&\& o \=\= \*n \+ 5: SUCCESS +\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/test_scalar_memory_replace/test.desc b/regression/contracts/test_scalar_memory_replace/test.desc index 5a00ec342ff..d85dbb8f05d 100644 --- a/regression/contracts/test_scalar_memory_replace/test.desc +++ b/regression/contracts/test_scalar_memory_replace/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ \[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS \[main.assertion.\d+\] line \d+ assertion \_\_CPROVER\_r\_ok\(n, sizeof\(int\)\): SUCCESS -\[main.assertion.\d+\] line \d+ assertion o \>\= 10 \&\& o \=\= \*n \+ 5: SUCCESS +\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/test_struct_enforce/test.desc b/regression/contracts/test_struct_enforce/test.desc index 077284e4885..d599fbdd40d 100644 --- a/regression/contracts/test_struct_enforce/test.desc +++ b/regression/contracts/test_struct_enforce/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS -\[foo.\d+\] line \d+ Check that x-\>baz is assignable: SUCCESS -\[foo.\d+\] line \d+ Check that x-\>qux is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that x->baz is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that x->qux is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion rval \=\= 10: SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/test_struct_member_enforce/test.desc b/regression/contracts/test_struct_member_enforce/test.desc index 439136d614d..80b4bf25076 100644 --- a/regression/contracts/test_struct_member_enforce/test.desc +++ b/regression/contracts/test_struct_member_enforce/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS -\[foo.\d+\] line \d+ Check that x-\>str\[\(.*\)\(x-\>len - 1\)\] is assignable: SUCCESS +\[foo.\d+\] line \d+ Check that x->str\[\(.*\)\(x->len - 1\)\] is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion rval \=\= 128: SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/test_struct_replace/test.desc b/regression/contracts/test_struct_replace/test.desc index ee71de5385d..e602d1a0787 100644 --- a/regression/contracts/test_struct_replace/test.desc +++ b/regression/contracts/test_struct_replace/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS -\[main.assertion.\d+\] line \d+ assertion rval \=\= x-\>baz \+ x-\>qux: SUCCESS +\[main.assertion.\d+\] line \d+ assertion rval \=\= x->baz \+ x->qux: SUCCESS \[main.assertion.\d+\] line \d+ assertion \*x \=\= \*y: SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/trivial_contract_enforce/test.desc b/regression/contracts/trivial_contract_enforce/test.desc index 6152a27cbcc..7c3f3219e3b 100644 --- a/regression/contracts/trivial_contract_enforce/test.desc +++ b/regression/contracts/trivial_contract_enforce/test.desc @@ -3,7 +3,7 @@ main.c --enforce-all-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.\d+\] line \d+ assertion foo\(\&n\) != 15\: FAILURE$ +^\[main.assertion.\d+\] line \d+ assertion foo\(\&n\) != 15: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/trivial_contract_replace/test.desc b/regression/contracts/trivial_contract_replace/test.desc index ce065cb1fe6..fa5772d02e8 100644 --- a/regression/contracts/trivial_contract_replace/test.desc +++ b/regression/contracts/trivial_contract_replace/test.desc @@ -3,7 +3,7 @@ main.c --enforce-all-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main.assertion.\d+\] line \d+ assertion foo\(\&n\) != 15\: FAILURE$ +^\[main.assertion.\d+\] line \d+ assertion foo\(\&n\) != 15: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index 31966c6202e..9f8a9aae503 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -24,49 +24,32 @@ assigns_clause_targett::assigns_clause_targett( code_contractst &contract, messaget &log_parameter, const irep_idt &function_id) - : pointer_object(pointer_for(object)), - contract(contract), + : contract(contract), init_block(), log(log_parameter), - target(typet()), + target(pointer_for(object)), target_id(object.id()) { INVARIANT( - pointer_object.type().id() == ID_pointer, + target.type().id() == ID_pointer, "Assigns clause targets should be stored as pointer expressions."); - const symbolt &function_symbol = contract.ns.lookup(function_id); - - // Declare a new symbol to stand in for the reference - symbolt standin_symbol = contract.new_tmp_symbol( - pointer_object.type(), - function_symbol.location, - function_symbol.mode); - - target = standin_symbol.symbol_expr(); - - // Build standin variable initialization block - init_block.add(goto_programt::make_decl(target, function_symbol.location)); - init_block.add(goto_programt::make_assignment( - code_assignt(target, pointer_object), function_symbol.location)); } assigns_clause_targett::~assigns_clause_targett() { } -std::vector assigns_clause_targett::temporary_declarations() const -{ - std::vector result; - result.push_back(target); - return result; -} - exprt assigns_clause_targett::alias_expression(const exprt &lhs) { exprt::operandst condition; exprt lhs_ptr = (lhs.id() == ID_address_of) ? to_address_of_expr(lhs).object() : pointer_for(lhs); + // __CPROVER_w_ok(target, sizeof(target)) + condition.push_back(w_ok_exprt( + target, + size_of_expr(dereference_exprt(target).type(), contract.ns).value())); + // __CPROVER_same_object(lhs, target) condition.push_back(same_object(lhs_ptr, target)); @@ -103,17 +86,12 @@ exprt assigns_clause_targett::alias_expression(const exprt &lhs) exprt assigns_clause_targett::compatible_expression( const assigns_clause_targett &called_target) { - return same_object(called_target.get_direct_pointer(), target); -} - -const exprt &assigns_clause_targett::get_direct_pointer() const -{ - return pointer_object; + return same_object(called_target.get_target(), target); } -goto_programt &assigns_clause_targett::get_init_block() +const exprt &assigns_clause_targett::get_target() const { - return init_block; + return target; } assigns_clauset::assigns_clauset( @@ -140,7 +118,7 @@ assigns_clauset::~assigns_clauset() } } -assigns_clause_targett *assigns_clauset::add_target(exprt target) +void assigns_clauset::add_target(exprt target) { assigns_clause_targett *new_target = new assigns_clause_targett( (target.id() == ID_address_of) @@ -150,42 +128,13 @@ assigns_clause_targett *assigns_clauset::add_target(exprt target) log, function_id); targets.push_back(new_target); - return new_target; -} - -goto_programt assigns_clauset::init_block() -{ - goto_programt result; - for(assigns_clause_targett *target : targets) - { - for(goto_programt::instructiont inst : - target->get_init_block().instructions) - { - result.add(goto_programt::instructiont(inst)); - } - } - return result; -} - -goto_programt assigns_clauset::dead_stmts() -{ - goto_programt dead_statements; - for(assigns_clause_targett *target : targets) - { - for(symbol_exprt symbol : target->temporary_declarations()) - { - dead_statements.add( - goto_programt::make_dead(symbol, symbol.source_location())); - } - } - return dead_statements; } goto_programt assigns_clauset::havoc_code() { modifiest modifies; for(const auto &t : targets) - modifies.insert(to_address_of_expr(t->get_direct_pointer()).object()); + modifies.insert(to_address_of_expr(t->get_target()).object()); goto_programt havoc_statements; append_havoc_code(assigns.source_location(), modifies, havoc_statements); @@ -231,7 +180,7 @@ exprt assigns_clauset::compatible_expression( // Validating the called target through __CPROVER_w_ok() is // only useful when the called target is a dereference - const auto &called_target_ptr = called_target->get_direct_pointer(); + const auto &called_target_ptr = called_target->get_target(); if( to_address_of_expr(called_target_ptr).object().id() == ID_dereference) { diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h index d1a631cfc39..b5a380ec1ef 100644 --- a/src/goto-instrument/contracts/assigns.h +++ b/src/goto-instrument/contracts/assigns.h @@ -29,11 +29,9 @@ class assigns_clause_targett const irep_idt &function_id); ~assigns_clause_targett(); - std::vector temporary_declarations() const; exprt alias_expression(const exprt &lhs); exprt compatible_expression(const assigns_clause_targett &called_target); - const exprt &get_direct_pointer() const; - goto_programt &get_init_block(); + const exprt &get_target() const; static exprt pointer_for(const exprt &object) { @@ -41,11 +39,10 @@ class assigns_clause_targett } protected: - const exprt pointer_object; const code_contractst &contract; goto_programt init_block; messaget &log; - symbol_exprt target; + exprt target; const irep_idt &target_id; }; @@ -59,9 +56,7 @@ class assigns_clauset messaget log_parameter); ~assigns_clauset(); - assigns_clause_targett *add_target(exprt target); - goto_programt init_block(); - goto_programt dead_stmts(); + void add_target(exprt target); goto_programt havoc_code(); exprt alias_expression(const exprt &lhs); exprt compatible_expression(const assigns_clauset &called_assigns); diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 2991855f781..6f9a1c35018 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -750,11 +750,7 @@ void code_contractst::instrument_call_statement( typet cast_type = rhs.type(); // Make freshly allocated memory assignable, if we can determine its type. - assigns_clause_targett *new_target = - assigns_clause.add_target(dereference_exprt(rhs)); - goto_programt &pointer_capture = new_target->get_init_block(); - insert_before_swap_and_advance( - program, instruction_iterator, pointer_capture); + assigns_clause.add_target(dereference_exprt(rhs)); } return; // assume malloc edits no pre-existing memory objects. } @@ -895,10 +891,6 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) return true; } goto_programt &program = old_function->second.body; - if(program.instructions.empty()) // empty function body - { - return false; - } if(check_for_looped_mallocs(program)) { @@ -923,17 +915,9 @@ void code_contractst::check_frame_conditions( // Create a list of variables that are okay to assign. std::set freely_assignable_symbols; - // Create temporary variables to hold the assigns - // clause targets before they can be modified. - goto_programt standin_decls = assigns.init_block(); - // Create dead statements for temporary variables - goto_programt mark_dead = assigns.dead_stmts(); - - // Skip lines with temporary variable declarations - auto instruction_it = program.instructions.begin(); - insert_before_swap_and_advance(program, instruction_it, standin_decls); - - for(; instruction_it != program.instructions.end(); ++instruction_it) + for(auto instruction_it = program.instructions.begin(); + instruction_it != program.instructions.end(); + ++instruction_it) { if(instruction_it->is_decl()) { @@ -941,15 +925,7 @@ void code_contractst::check_frame_conditions( freely_assignable_symbols.insert( instruction_it->get_decl().symbol().get_identifier()); - assigns_clause_targett *new_target = - assigns.add_target(instruction_it->get_decl().symbol()); - goto_programt &pointer_capture = new_target->get_init_block(); - - for(auto in : pointer_capture.instructions) - { - program.insert_after(instruction_it, in); - ++instruction_it; - } + assigns.add_target(instruction_it->get_decl().symbol()); } else if(instruction_it->is_assign()) { @@ -970,15 +946,6 @@ void code_contractst::check_frame_conditions( assigns); } } - - // Walk the iterator back to the last statement - while(!instruction_it->is_end_function()) - { - --instruction_it; - } - - // Make sure the temporary symbols are marked dead - program.insert_before_swap(instruction_it, mark_dead); } bool code_contractst::enforce_contract(const irep_idt &function)