Add tests for shadow memory via nondet struct accesses

Checks that shadow memory accesses are not confused
by potentially nondeterministic accesses into structs.

Author: peterschrammel

regression/cbmc-shadow-memory/nondet-pointer-into-struct1/main.c

@@ -0,0 +1,61 @@
+#include <assert.h>
+
+struct STRUCTNAME
+{
+  int x1;
+  int x2;
+};
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (char)0);
+
+  struct STRUCTNAME n, m;
+  int *p, *q;
+
+  // Goto-symex is expected to create a case split for dereferencing p and q.
+  int choice;
+  __CPROVER_assume(choice > 0);
+  if(choice)
+  {
+    p = &m.x1;
+    q = &m.x2;
+  }
+  else
+  {
+    p = &n.x1;
+    q = &n.x2;
+  }
+
+  assert(__CPROVER_get_field(&m.x1, "field1") == 0);
+  assert(__CPROVER_get_field(&m.x2, "field1") == 0);
+  assert(__CPROVER_get_field(p, "field1") == 0);
+  assert(__CPROVER_get_field(q, "field1") == 0);
+
+  __CPROVER_set_field(&m.x1, "field1", 2);
+  assert(__CPROVER_get_field(&m.x1, "field1") == 2);
+  assert(__CPROVER_get_field(&m.x2, "field1") == 0);
+  assert(__CPROVER_get_field(p, "field1") == 2);
+  assert(__CPROVER_get_field(q, "field1") == 0);
+
+  __CPROVER_set_field(&m.x2, "field1", 3);
+  assert(__CPROVER_get_field(&m.x1, "field1") == 2);
+  assert(__CPROVER_get_field(&m.x2, "field1") == 3);
+  assert(__CPROVER_get_field(p, "field1") == 2);
+  assert(__CPROVER_get_field(q, "field1") == 3);
+
+  __CPROVER_set_field(p, "field1", 4);
+  assert(__CPROVER_get_field(&m.x1, "field1") == 4);
+  assert(__CPROVER_get_field(&m.x2, "field1") == 3);
+  assert(__CPROVER_get_field(p, "field1") == 4);
+  assert(__CPROVER_get_field(q, "field1") == 3);
+
+  __CPROVER_set_field(q, "field1", 5);
+  assert(__CPROVER_get_field(&m.x1, "field1") == 4);
+  assert(__CPROVER_get_field(&m.x2, "field1") == 5);
+  assert(__CPROVER_get_field(p, "field1") == 4);
+  assert(__CPROVER_get_field(q, "field1") == 5);
+
+  assert(__CPROVER_get_field(&n.x1, "field1") == 0);
+  assert(__CPROVER_get_field(&n.x2, "field1") == 0);
+}

regression/cbmc-shadow-memory/nondet-pointer-into-struct1/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring