No need to track write set with temporary variables

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$
 --
 --

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$
 --
 --

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$
 --
 --

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$
 --
 --

regression/contracts/assigns_enforce_structs_07/main.c

@@ -0,0 +1,34 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+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;
+}

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.

regression/contracts/assigns_replace_07/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+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;
+}

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.

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$

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
 --

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

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

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:

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:

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:

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:

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$
 --
 --

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$
 --
 --

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$
 --
 --

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$
 --
 --

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$
 --

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$
 --
 --

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$
 --
 --

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$
 --

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$
 --

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$
 --

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$
 --
 --

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$
 --
 --