Adds memory-primitive flag to contracts regression tests

CBMC relies on memory primitives to check frame conditions.
We should ensure that regression tests for contracts do not
use these primitives with invalid pointers.

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/assigns_enforce_16/test.desc

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

regression/contracts/assigns_replace_03/main.c

@@ -1,17 +1,18 @@
 #include <assert.h>
+#include <stdlib.h>
 
 int y;
 double z;
 
-void bar(char **c) __CPROVER_assigns(y, z, **c) __CPROVER_ensures(**c == 6)
+void bar(char *c) __CPROVER_assigns(y, z, *c) __CPROVER_ensures(*c == 6)
 {
 }
 
 int main()
 {
-  char **b;
+  char *b = malloc(sizeof(*b));
   bar(b);
-  assert(**b == 6);
+  assert(*b == 6);
 
   return 0;
 }

regression/contracts/assigns_replace_03/test.desc

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

regression/contracts/assigns_type_checking_valid_cases/main.c

@@ -45,8 +45,7 @@ void foo5(struct buf buffer) __CPROVER_assigns(buffer)
   buffer.len = 0;
 }
 
-void foo6(struct buf *buffer)
-  __CPROVER_assigns(buffer->data, *(buffer->data), buffer->len)
+void foo6(struct buf *buffer) __CPROVER_assigns(buffer->data, buffer->len)
 {
   buffer->data = malloc(sizeof(*(buffer->data)));
   *(buffer->data) = 1;

regression/contracts/assigns_type_checking_valid_cases/test.desc

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