Add shadow memory pointer check regression tests

Author: Enrico Steffinlongo

regression/cbmc-shadow-memory/pointer-checks1/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+extern _Bool nondet();
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+
+  char *buffer[10];
+
+  __CPROVER_set_field(&buffer[9], "field1", 1);
+  assert(__CPROVER_get_field(&buffer[9], "field1") == 1);
+  __CPROVER_set_field(&buffer[10], "field1", 1);
+  if(nondet())
+  {
+    assert(__CPROVER_get_field(&buffer[10], "field1") == 1);
+  }
+}

regression/cbmc-shadow-memory/pointer-checks1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--verbosity 10 --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+line 13 dereference failure: pointer outside object bounds.*: FAILURE
+line 16 dereference failure: pointer outside object bounds.*: FAILURE
+--
+^warning: ignoring
+line 11 dereference failure: pointer outside object bounds.*: FAILURE
+line 12 dereference failure: pointer outside object bounds.*: FAILURE

regression/cbmc-shadow-memory/pointer-checks2/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("uninitialized", (char)0);
+
+  char a;
+  int *i = &a;
+
+  __CPROVER_set_field(i, "uninitialized", 1); // should this fail?
+
+  assert(__CPROVER_get_field(&a, "uninitialized") == 1);
+  assert(__CPROVER_get_field(&a + 1, "uninitialized") == 1);
+  assert(__CPROVER_get_field(i, "uninitialized") == 1);
+}

regression/cbmc-shadow-memory/pointer-checks2/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--verbosity 10 --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+line 10 dereference failure: pointer outside object bounds in \*i.*: FAILURE
+line 13 dereference failure: pointer outside object bounds in \(&a\).*: FAILURE
+line 14 dereference failure: pointer outside object bounds in \*i.*: FAILURE
+--