CONTRACTS: Dynamic frame condition checking

regression/contracts/assigns-enforce-malloc-zero/main.c

@@ -6,7 +6,7 @@ int foo(char *a, int size)
   // clang-format off
   __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
   __CPROVER_requires(a == NULL || __CPROVER_is_fresh(a, size))
-  __CPROVER_assigns(a: __CPROVER_POINTER_OBJECT(a))
+  __CPROVER_assigns(a: __CPROVER_whole_object(a))
   __CPROVER_ensures(
     a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
 // clang-format on

regression/contracts/assigns-enforce-malloc-zero/test.desc

@@ -1,7 +1,6 @@
 CORE
 main.c
---enforce-contract foo _ --malloc-may-fail --malloc-fail-null
-^\[foo.assigns.\d+\] line 9 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid when a != \(\(char \*\)NULL\): SUCCESS$
+--dfcc main --enforce-contract foo _ --malloc-may-fail --malloc-fail-null
 ^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$

regression/contracts/assigns-local-composite/test.desc

@@ -1,12 +1,12 @@
 CORE
 main.c
---enforce-contract foo
+--dfcc main --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Checks that assigns clause checking explicitly checks assignments to locally 
+Checks that assigns clause checking explicitly checks assignments to locally
 declared symbols with composite types, when they are dirty.
-Out of bounds accesses to locally declared arrays, structs, etc. 
+Out of bounds accesses to locally declared arrays, structs, etc.
 will be detected by assigns clause checking.

regression/contracts/assigns-replace-ignored-return-value/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
+--dfcc main --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns-replace-malloc-zero/main.c

@@ -6,7 +6,7 @@ int foo(char *a, int size)
   // clang-format off
 __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
 __CPROVER_requires(a == NULL || __CPROVER_rw_ok(a, size))
-__CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
+__CPROVER_assigns(__CPROVER_whole_object(a))
 __CPROVER_ensures(
     a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
 // clang-format on

regression/contracts/assigns-replace-malloc-zero/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null
+--dfcc main --replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$

regression/contracts/assigns-slice-targets/main-enforce.c

@@ -7,11 +7,14 @@ struct st
   int c;
 };
 
-void foo(struct st *s)
+void foo(struct st *s, struct st *ss)
   // clang-format off
   __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s)))
-  __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5))
-  __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5))
+  __CPROVER_assigns(
+    __CPROVER_object_upto(s->arr1, 5);
+    __CPROVER_object_from(s->arr2 + 5);
+    __CPROVER_whole_object(ss);
+)
 // clang-format on
 {
   // PASS
@@ -41,13 +44,24 @@ void foo(struct st *s)
   s->arr2[7] = 0;
   s->arr2[8] = 0;
   s->arr2[9] = 0;
+
+  // PASS
+  ss->a = 0;
+  ss->arr1[0] = 0;
+  ss->arr1[7] = 0;
+  ss->arr1[9] = 0;
+  ss->b = 0;
+  ss->arr2[6] = 0;
+  ss->arr2[8] = 0;
+  ss->c = 0;
 }
 
 int main()
 {
   struct st s;
+  struct st ss;
 
-  foo(&s);
+  foo(&s, &ss);
 
   return 0;
 }

regression/contracts/assigns-slice-targets/main-replace.c

@@ -7,11 +7,14 @@ struct st
   int c;
 };
 
-void foo(struct st *s)
+void foo(struct st *s, struct st *ss)
   // clang-format off
   __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s)))
-  __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5))
-  __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5))
+  __CPROVER_assigns(
+    __CPROVER_object_upto(s->arr1, 5);
+    __CPROVER_object_from(s->arr2 + 5);
+    __CPROVER_whole_object(ss);
+  )
 // clang-format on
 {
   s->arr1[0] = 0;
@@ -54,7 +57,32 @@ int main()
   s.arr2[9] = 0;
   s.c = 0;
 
-  foo(&s);
+  struct st ss;
+  ss.a = 0;
+  ss.arr1[0] = 0;
+  ss.arr1[1] = 0;
+  ss.arr1[2] = 0;
+  ss.arr1[3] = 0;
+  ss.arr1[4] = 0;
+  ss.arr1[5] = 0;
+  ss.arr1[6] = 0;
+  ss.arr1[7] = 0;
+  ss.arr1[8] = 0;
+  ss.arr1[9] = 0;
+
+  ss.arr2[0] = 0;
+  ss.arr2[1] = 0;
+  ss.arr2[2] = 0;
+  ss.arr2[3] = 0;
+  ss.arr2[4] = 0;
+  ss.arr2[5] = 0;
+  ss.arr2[6] = 0;
+  ss.arr2[7] = 0;
+  ss.arr2[8] = 0;
+  ss.arr2[9] = 0;
+  ss.c = 0;
+
+  foo(&s, &ss);
 
   // PASS
   assert(s.a == 0);
@@ -92,5 +120,31 @@ int main()
 
   // PASS
   assert(s.c == 0);
+
+  // FAIL
+  assert(ss.a == 0);
+  assert(ss.arr1[0] == 0);
+  assert(ss.arr1[1] == 0);
+  assert(ss.arr1[2] == 0);
+  assert(ss.arr1[3] == 0);
+  assert(ss.arr1[4] == 0);
+  assert(ss.arr1[5] == 0);
+  assert(ss.arr1[6] == 0);
+  assert(ss.arr1[7] == 0);
+  assert(ss.arr1[8] == 0);
+  assert(ss.arr1[9] == 0);
+  assert(ss.b == 0);
+  assert(ss.arr2[0] == 0);
+  assert(ss.arr2[1] == 0);
+  assert(ss.arr2[2] == 0);
+  assert(ss.arr2[3] == 0);
+  assert(ss.arr2[4] == 0);
+  assert(ss.arr2[5] == 0);
+  assert(ss.arr2[6] == 0);
+  assert(ss.arr2[7] == 0);
+  assert(ss.arr2[8] == 0);
+  assert(ss.arr2[9] == 0);
+  assert(ss.c == 0);
+
   return 0;
 }

regression/contracts/assigns-slice-targets/test-enforce.desc

@@ -1,8 +1,6 @@
 CORE
 main-enforce.c
---enforce-contract foo
-^\[foo.assigns.\d+\].* Check that __CPROVER_object_slice\(\(void \*\)s->arr1, \(.*\)5\) is valid: SUCCESS$
-^\[foo.assigns.\d+\].* Check that __CPROVER_object_from\(\(void \*\)\(s->arr2 \+ \(.*\)5\)\) is valid: SUCCESS$
+--dfcc main --enforce-contract foo
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$
@@ -23,6 +21,14 @@ main-enforce.c
 ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->a is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)7\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)9\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->b is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)6\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)8\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->c is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts/assigns-slice-targets/test-replace.desc

@@ -1,6 +1,6 @@
 CORE
 main-replace.c
---replace-call-with-contract foo
+--dfcc main --replace-call-with-contract foo
 ^\[main.assertion.\d+\].*assertion s.a == 0: SUCCESS$
 ^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)0\] == 0: FAILURE$
 ^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)1\] == 0: FAILURE$
@@ -24,6 +24,29 @@ main-replace.c
 ^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)8\] == 0: FAILURE$
 ^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)9\] == 0: FAILURE$
 ^\[main.assertion.\d+\].*assertion s.c == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion ss.a == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)0\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)1\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)2\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)3\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)4\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)5\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)6\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)7\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)8\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)9\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion ss.b == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)0\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)1\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)2\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)3\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)4\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)5\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)6\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)7\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)8\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)9\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion ss.c == 0: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_01/test.desc

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