Propagate write-set checks to sub-functions

regression/contracts/assigns_enforce_01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_04/test.desc

@@ -1,9 +1,18 @@
 CORE
 main.c
---enforce-all-contracts
-^EXIT=10$
+--enforce-contract f1
+^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
+^\[f1.\d+\] line \d+ Check that x2 is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that y2 is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that z2 is assignable: SUCCESS$
+^\[f2.\d+\] line \d+ Check that x3 is assignable: SUCCESS$
+^\[f2.\d+\] line \d+ Check that y3 is assignable: SUCCESS$
+^\[f2.\d+\] line \d+ Check that z3 is assignable: SUCCESS$
+^\[f3.\d+\] line \d+ Check that \*x3 is assignable: SUCCESS$
+^\[f3.\d+\] line \d+ Check that \*y3 is assignable: SUCCESS$
+^\[f3.\d+\] line \d+ Check that \*z3 is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks that verification fails when an assigns clause is not respected through multiple function calls.
+This test checks that verification only considers assigns clause from enforced function.

regression/contracts/assigns_enforce_05/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f1.1\] line \d+ .*: SUCCESS$

regression/contracts/assigns_enforce_06/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_07/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_08/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_09/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_10/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_11/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_12/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_13/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_14/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_15/test.desc

@@ -1,11 +1,10 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo --enforce-contract baz --enforce-contract qux
 ^EXIT=10$
 ^SIGNAL=0$
-^\[bar\.1\] line \d+ .*: FAILURE$
-^\[baz\.1\] line \d+ .*: FAILURE$
-^\[qux\.1\] line \d+ .*: FAILURE$
+^\[baz.\d+\] line \d+ Check that global is assignable: FAILURE$
+^\[qux.\d+\] line \d+ Check that global is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_enforce_16/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts _ --pointer-primitive-check
+--enforce-contract foo _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_17/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract pure
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$

regression/contracts/assigns_enforce_18/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts _ --pointer-primitive-check
+--enforce-contract foo --enforce-contract bar --enforce-contract baz _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[bar.\d+\] line \d+ Check that \*a is assignable: SUCCESS$

regression/contracts/assigns_enforce_19/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f --enforce-contract g
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f.\d+\] line \d+ Check that a is assignable: SUCCESS$

regression/contracts/assigns_enforce_20/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[foo.\d+\] line \d+ Check that \*y is assignable: FAILURE$

regression/contracts/assigns_enforce_21/main.c

@@ -0,0 +1,42 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int x = 0;
+
+void quz() __CPROVER_assigns(x) __CPROVER_ensures(x == -1)
+{
+  x = -1;
+}
+
+int baz() __CPROVER_assigns()
+{
+  return 5;
+}
+
+void bar(int *y, int w) __CPROVER_assigns(*y)
+{
+  *y = 3;
+  w = baz();
+  assert(w == 5);
+  quz();
+}
+
+void foo(int *y, int z) __CPROVER_assigns(*y)
+{
+  int w = 5;
+  assert(w == 5);
+  bar(y, w);
+  z = -2;
+}
+
+int main()
+{
+  int *y = malloc(sizeof(*y));
+  *y = 0;
+  int z = 1;
+  foo(y, z);
+  assert(x == -1);
+  assert(*y == 3);
+  assert(z == 1);
+  return 0;
+}

regression/contracts/assigns_enforce_21/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--enforce-contract foo --replace-call-with-contract quz
+^EXIT=10$
+^SIGNAL=0$
+main.c function bar
+^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
+^\[bar.\d+\] line \d+ Check that x is assignable: FAILURE$
+^\[baz.\d+\] line \d+ Check that w is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+Checks whether checks write set for sub-function calls.

regression/contracts/assigns_enforce_address_of/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int foo(int *x) __CPROVER_assigns(&x)
+{
+  *x = 0;
+  return 0;
+}
+
+int main()
+{
+  int x;
+  foo(&x);
+  return 0;
+}

regression/contracts/assigns_enforce_address_of/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=(1|64)$
+^SIGNAL=0$
+^.*error: illegal target in assigns clause$
+^CONVERSION ERROR$
+--
+--
+Check that address_of expressions are rejected in assigns clauses.

regression/contracts/assigns_enforce_arrays_01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_arrays_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract nextIdx
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_arrays_03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract assign_out_under
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_arrays_04/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract assigns_single --enforce-contract assigns_range --enforce-contract assigns_big_range
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_arrays_05/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract assigns_ptr --enforce-contract assigns_range
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_arrays_10/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract nextIdx
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_elvis_1/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int foo(bool a, int *x, int *y, int *z) __CPROVER_assigns(*(a ? x : y))
+{
+  if(a)
+    *x = 0; // must pass
+  else
+    *y = 0; // must pass
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+  int z;
+
+  foo(a, &x, &y, &z);
+  return 0;
+}

regression/contracts/assigns_enforce_elvis_1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+main.c function foo
+^\[foo.1] line \d+ Check that \*x is assignable: SUCCESS$
+^\[foo.2] line \d+ Check that \*y is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Check that Elvis operator expressions '*(cond ? if_true : if_false)' are accepted in assigns clauses and work as expected.

regression/contracts/assigns_enforce_elvis_2/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int foo(bool a, int *x, int *y, int *z) __CPROVER_assigns(*(a ? x : y))
+{
+  if(a)
+    *x = 0; // must pass
+  else
+    *z = 0; // must fail
+  return 0;
+}
+
+int main()
+{
+  bool a;
+  int x;
+  int y;
+  int z;
+
+  foo(a, &x, &y, &z);
+  return 0;
+}

regression/contracts/assigns_enforce_elvis_2/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=10$
+^SIGNAL=0$
+main.c function foo
+^\[foo.1] line \d+ Check that \*x is assignable: SUCCESS$
+^\[foo.2] line \d+ Check that \*z is assignable: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Check that Elvis operator expressions '*(cond ? if_true : if_false)' are accepted in assigns clauses and work as expected.