Merge pull request #6377 from feliperodri/car

Author: feliperodri

regression/contracts/assigns_enforce_18/test.desc

@@ -3,21 +3,18 @@ main.c
 --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$
+^\[bar.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
-^\[baz.\d+\] line \d+ Check that \*c is assignable: FAILURE$
+^\[baz.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$
 ^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
-^.* 2 of \d+ failed \(\d+ iteration.*\)$
+^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
-^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$
-^\[foo.pointer\_primitives.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(tmp\_cc\$\d+\): FAILURE$
-^.* 3 of \d+ failed (\d+ iterations)$
 --
 Checks whether contract enforcement works with functions that deallocate memory.
 We had problems before when freeing a variable, but still keeping it on

regression/contracts/assigns_enforce_23/main.c

@@ -0,0 +1,41 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+typedef struct
+{
+  uint8_t *buf;
+  size_t size;
+} blob;
+
+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_ensures(b->buf[0] == 1)
+__CPROVER_ensures(b->buf[1] == 1)
+__CPROVER_ensures(b->buf[2] == 1)
+__CPROVER_ensures(b->buf[3] == 1)
+__CPROVER_ensures(b->buf[4] == 1)
+// clang-format on
+{
+  b->buf[0] = *value;
+  b->buf[1] = *value;
+  b->buf[2] = *value;
+  b->buf[3] = *value;
+  b->buf[4] = *value;
+
+  *value = 2;
+}
+
+int main()
+{
+  blob b;
+  b.size = 5;
+  b.buf = malloc(b.size * (sizeof(*(b.buf))));
+  uint8_t value = 1;
+
+  foo(&b, &value);
+
+  return 0;
+}

regression/contracts/assigns_enforce_23/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that POINTER_OBJECT can be used both on arrays and scalars.

regression/contracts/assigns_enforce_arrays_02/main.c

@@ -1,24 +1,24 @@
 #include <assert.h>
+#include <stdlib.h>
 
-int idx = 4;
+int *arr;
 
-int nextIdx() __CPROVER_assigns(idx)
+void f1(int *a, int len) __CPROVER_assigns(*a)
 {
-  idx++;
-  return idx;
+  a[0] = 0;
+  a[5] = 5;
 }
 
-void f1(int a[], int len) __CPROVER_assigns(*a, idx)
+void f2(int *a, int len) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
 {
-  a[nextIdx()] = 5;
+  a[0] = 0;
+  a[5] = 5;
+  free(a);
 }
 
 int main()
 {
-  int arr[10];
-  f1(arr, 10);
-
-  assert(idx == 5);
-
-  return 0;
+  arr = malloc(100 * sizeof(int));
+  f1(arr, 100);
+  f2(arr, 100);
 }

regression/contracts/assigns_enforce_arrays_02/test.desc

@@ -1,14 +1,15 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract nextIdx
-^EXIT=0$
+--enforce-contract f1 --enforce-contract f2
+^\[f1.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that a\[.*5\] is assignable: FAILURE$
+^\[f2.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
+^\[f2.\d+\] line \d+ Check that a\[.*5\] is assignable: SUCCESS$
+^\[f2.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 --
 --
-Checks whether the instrumentation process does not duplicate function calls
-used as part of array-index operations, i.e., if a function call is used in
-the computation of the index of an array assignment, then instrumenting that
-statement with an assigns clause will not result in multiple function calls.
-This test also ensures that assigns clauses correctly check for global
-variables modified by subcalls.
+This test ensures that assigns clauses correctly check for global variables,
+and access using *ptr vs POINTER_OBJECT(ptr).

regression/contracts/assigns_enforce_elvis_5/test.desc

@@ -8,3 +8,5 @@ main.c
 --
 Check that Elvis operator expressions of form '(cond ? *if_true : *if_false)'
 are supported in assigns clauses.
+
+BUG: `is_lvalue` in goto is not consistent with `target.get_bool(ID_C_lvalue)`.

regression/contracts/assigns_enforce_function_calls/main.c

@@ -17,5 +17,5 @@ int main()
 {
   int x;
   foo(&x);
-  return 0;
+  baz(&x);
 }

regression/contracts/assigns_enforce_function_calls/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: Assigns clause is not side-effect free.$
+^.*error: illegal target in assigns clause$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_object_wrong_args/main.c

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

regression/contracts/assigns_enforce_object_wrong_args/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract baz
+^EXIT=(1|64)$
+^SIGNAL=0$
+^.*error: pointer_object expects one argument$
+^CONVERSION ERROR$
+--
+--
+Check that `__CPROVER_POINTER_OBJECT` in assigns clauses are invoked correctly.