Adds memory-primitive check to contracts regression

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_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_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/chain.sh

@@ -44,4 +44,4 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
   rm "${name}-mod.c"
 fi
 $goto_instrument --show-goto-functions "${name}-mod.gb"
-$cbmc "${name}-mod.gb" ${args_cbmc}
+$cbmc "${name}-mod.gb" ${args_cbmc} --pointer-primitive-check