Merge pull request #7086 from remi-delmas-3000/assignable_t-builtins-…

…frees-clause

CONTRACTS: Front-end extensions for assigns clauses

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_object_whole(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,7 @@
 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$
+^\[foo.assigns.\d+\] line 9 Check that __CPROVER_object_whole\(\(.* \*\)a\) is valid when a != \(\(.* \*\)NULL\): SUCCESS$
 ^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$

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_object_whole(a))
 __CPROVER_ensures(
     a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
 // clang-format on

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_object_whole(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_object_whole(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$
 ^\[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

@@ -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_23/main.c

@@ -10,8 +10,8 @@ typedef struct
 void foo(blob *b, uint8_t *value)
   // clang-format off
 __CPROVER_requires(b->size == 5)
-__CPROVER_assigns(__CPROVER_POINTER_OBJECT(b->buf))
-__CPROVER_assigns(__CPROVER_POINTER_OBJECT(value))
+__CPROVER_assigns(__CPROVER_object_whole(b->buf))
+__CPROVER_assigns(__CPROVER_object_whole(value))
 __CPROVER_ensures(b->buf[0] == 1)
 __CPROVER_ensures(b->buf[1] == 1)
 __CPROVER_ensures(b->buf[2] == 1)

regression/contracts/assigns_enforce_23/test.desc

@@ -6,4 +6,4 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks that POINTER_OBJECT can be used both on arrays and scalars.
+This test checks that __CPROVER_object_whole can be used both on arrays and scalars.

regression/contracts/assigns_enforce_address_of/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_arrays_02/main.c

@@ -9,7 +9,7 @@ void f1(int *a, int len) __CPROVER_assigns(*a)
   a[5] = 5;
 }
 
-void f2(int *a, int len) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
+void f2(int *a, int len) __CPROVER_assigns(__CPROVER_object_whole(a))
 {
   a[0] = 0;
   a[5] = 5;

regression/contracts/assigns_enforce_arrays_02/test.desc

@@ -4,14 +4,14 @@ main.c
 ^\[f1.assigns.\d+\] line 6 Check that \*a is valid: SUCCESS$
 ^\[f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$
 ^\[f1.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$
-^\[f2.assigns.\d+\] line 12 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid: SUCCESS$
+^\[f2.assigns.\d+\] line 12 Check that __CPROVER_object_whole\(\(.* \*\)a\) is valid: SUCCESS$
 ^\[f2.assigns.\d+\] line 14 Check that a\[.*0\] is assignable: SUCCESS$
 ^\[f2.assigns.\d+\] line 15 Check that a\[.*5\] is assignable: SUCCESS$
-^\[f2.assigns.\d+\] line 16 Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
+^\[f2.assigns.\d+\] line 16 Check that POINTER_OBJECT\(\(.* \*\)a\) is assignable: SUCCESS$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
 --
 This test ensures that assigns clauses correctly check for global variables,
-and access using *ptr vs POINTER_OBJECT(ptr).
+and access using *ptr vs __CPROVER_object_whole(ptr).

regression/contracts/assigns_enforce_arrays_04/main.c

@@ -5,8 +5,7 @@ void assigns_single(int a[], int len)
   a[i] = 0;
 }
 
-void uses_assigns(int a[], int len)
-  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
+void uses_assigns(int a[], int len) __CPROVER_assigns(__CPROVER_object_whole(a))
 {
   assigns_single(a, len);
 }

regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_pointer_object/main.c

@@ -3,8 +3,8 @@
 int foo(bool a, char *x, char *y)
   // clang-format off
  __CPROVER_assigns(
-    a: __CPROVER_POINTER_OBJECT(x);
-   !a: __CPROVER_POINTER_OBJECT(y);
+    a: __CPROVER_object_whole(x);
+   !a: __CPROVER_object_whole(y);
   )
 // clang-format on
 {

regression/contracts/assigns_enforce_conditional_pointer_object/test.desc

@@ -2,8 +2,8 @@ CORE
 main.c
 --enforce-contract foo
 main.c function foo
-^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)x\) is valid when a != FALSE: SUCCESS$
-^\[foo.assigns.\d+\] line 7 Check that POINTER_OBJECT\(\(const void \*\)y\) is valid when !\(a != FALSE\): SUCCESS$
+^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.* \*\)x\) is valid when a != FALSE: SUCCESS$
+^\[foo.assigns.\d+\] line 7 Check that __CPROVER_object_whole\(\(.* \*\)y\) is valid when !\(a != FALSE\): SUCCESS$
 ^\[foo.assigns.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
 ^\[foo.assigns.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
@@ -15,5 +15,5 @@ main.c function foo
 ^SIGNAL=0$
 --
 --
-Check that conditional assigns clause  `c ? __CPROVER_POINTER_OBJECT((p)`
+Check that conditional assigns clause  `c ? __CPROVER_object_whole((p)`
 match with control flow path conditions.

regression/contracts/assigns_enforce_conditional_pointer_object_list/main.c

@@ -3,7 +3,7 @@
 int foo(bool a, char *x, char *y)
   // clang-format off
 __CPROVER_assigns(
-   a : __CPROVER_POINTER_OBJECT(x), __CPROVER_POINTER_OBJECT(y)
+   a : __CPROVER_object_whole(x), __CPROVER_object_whole(y)
 )
 // clang-format on
 {

regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc

@@ -2,8 +2,8 @@ CORE
 main.c
 --enforce-contract foo
 main.c function foo
-^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)x\) is valid when a != FALSE: SUCCESS$
-^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)y\) is valid when a != FALSE: SUCCESS$
+^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.*\)x\) is valid when a != FALSE: SUCCESS$
+^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.*\)y\) is valid when a != FALSE: SUCCESS$
 ^\[foo.assigns.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$

regression/contracts/assigns_enforce_conditional_unions/main.c

@@ -70,10 +70,10 @@ __CPROVER_requires(
               sizeof(*(state->digest.high_level.second.ctx->digest))))
 __CPROVER_assigns(
   is_high_level():
-    __CPROVER_POINTER_OBJECT(state->digest.high_level.first.ctx->digest),
+    __CPROVER_object_whole(state->digest.high_level.first.ctx->digest),
     state->digest.high_level.first.ctx->flags;
   is_high_level() && also_second:
-    __CPROVER_POINTER_OBJECT(state->digest.high_level.second.ctx->digest),  
+    __CPROVER_object_whole(state->digest.high_level.second.ctx->digest),  
     state->digest.high_level.second.ctx->flags;
 )
 // clang-format on

regression/contracts/assigns_enforce_conditional_unions/test.desc

@@ -1,9 +1,9 @@
 CORE
 main.c
 --enforce-contract update _ --pointer-check --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check --conversion-check
-^\[update.assigns.\d+] line 73 Check that POINTER_OBJECT\(\(const void \*\)state->digest.high_level.first.ctx->digest\) is valid when .*: SUCCESS
+^\[update.assigns.\d+] line 73 Check that __CPROVER_object_whole\(\(.*\)state->digest.high_level.first.ctx->digest\) is valid when .*: SUCCESS
 ^\[update.assigns.\d+] line 74 Check that state->digest.high_level.first.ctx->flags is valid when .*: SUCCESS
-^\[update.assigns.\d+] line 76 Check that POINTER_OBJECT\(\(const void \*\)state->digest.high_level.second.ctx->digest\) is valid when .*: SUCCESS
+^\[update.assigns.\d+] line 76 Check that __CPROVER_object_whole\(\(.*\)state->digest.high_level.second.ctx->digest\) is valid when .*: SUCCESS
 ^\[update.assigns.\d+] line 77 Check that state->digest.high_level.second.ctx->flags is valid when .*: SUCCESS
 ^\[is_high_level.assigns.\d+\] line 50 Check that latch is assignable: SUCCESS$
 ^\[is_high_level.assigns.\d+\] line 51 Check that once is assignable: SUCCESS$

regression/contracts/assigns_enforce_conditional_void_target/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.* error: (void-typed expressions not allowed as assigns clause targets|dereferencing void pointer)$
+^.* error: (dereferencing void pointer|lvalue expressions with void type not allowed in assigns clauses)$
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_void_target_list/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.* error: (void-typed expressions not allowed as assigns clause targets|dereferencing void pointer)$
+^.* error: (dereferencing void pointer|lvalue expressions with void type not allowed in assigns clauses)$
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_function_calls/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: function calls in assigns clause targets must be to __CPROVER_object_from, __CPROVER_object_slice$
+^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
 ^CONVERSION ERROR$
 --
 --