Add tests for shadow memory of linked lists

Test deterministic and nondeterministic pointers
to elements.

Author: peterschrammel

regression/cbmc-shadow-memory/linked-list1/main.c

@@ -0,0 +1,70 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct STRUCTNAME
+{
+  int data;
+  struct STRUCTNAME *next;
+};
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+
+  struct STRUCTNAME a;
+
+  assert(__CPROVER_get_field(&a, "field1") == 0);
+  assert(__CPROVER_get_field(&(a.data), "field1") == 0);
+  assert(__CPROVER_get_field(&(a.next), "field1") == 0);
+  // Expect a warning here. We return 0 as default value.
+  assert(__CPROVER_get_field(a.next, "field1") == 0);
+  // Expect a warning here. We return 0 as default value.
+  assert(__CPROVER_get_field((*(a.next)).next, "field1") == 0);
+
+  __CPROVER_set_field(&(a.data), "field1", 1);
+  __CPROVER_set_field(&(a.next), "field1", 1);
+  // Expect a warning here. We cannot set SM because it doesn't exist.
+  __CPROVER_set_field(&((*(a.next)).data), "field1", 1);
+  // Expect a warning here. We cannot set SM because it doesn't exist.
+  __CPROVER_set_field(&((*(*(a.next)).next).data), "field1", 1);
+
+  assert(__CPROVER_get_field(&a, "field1") == 1);
+  assert(__CPROVER_get_field(&(a.data), "field1") == 1);
+  assert(__CPROVER_get_field(&(a.next), "field1") == 1);
+  // Expect a warning here. We return 0 as default value.
+  assert(__CPROVER_get_field(a.next, "field1") == 0);
+  // Expect a warning here. We return 0 as default value.
+  assert(__CPROVER_get_field((*(a.next)).next, "field1") == 0);
+
+  struct STRUCTNAME b;
+  a.next = &b;
+
+  assert(__CPROVER_get_field(&a, "field1") == 1);
+  assert(__CPROVER_get_field(&(a.data), "field1") == 1);
+  assert(__CPROVER_get_field(&(a.next), "field1") == 1);
+  // No warning here.
+  assert(__CPROVER_get_field(a.next, "field1") == 0);
+  // Expect a warning here. We return 0 as default value.
+  assert(__CPROVER_get_field((*(a.next)).next, "field1") == 0);
+
+  // No warning here.
+  __CPROVER_set_field(&((*(a.next)).data), "field1", 1);
+  // Expect a warning here. We cannot set SM because it doesn't exist.
+  __CPROVER_set_field(&((*(*(a.next)).next).data), "field1", 1);
+
+  // No warning here.
+  assert(__CPROVER_get_field(a.next, "field1") == 1);
+  // Expect a warning here. We return 0 as default value.
+  assert(__CPROVER_get_field((*(a.next)).next, "field1") == 0);
+
+  struct STRUCTNAME c;
+  b.next = &c;
+  // No warning here.
+  assert(__CPROVER_get_field((*(a.next)).next, "field1") == 0);
+
+  // No warning here.
+  __CPROVER_set_field(&((*(*(a.next)).next).data), "field1", 1);
+
+  // No warning here.
+  assert(__CPROVER_get_field((*(a.next)).next, "field1") == 1);
+}

regression/cbmc-shadow-memory/linked-list1/test.desc

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

regression/cbmc-shadow-memory/linked-list2/main.c

@@ -0,0 +1,71 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct STRUCTNAME
+{
+  int data;
+  struct STRUCTNAME *next;
+};
+
+int main()
+{
+  int x;
+  int y;
+  __CPROVER_assume(x > 0);
+  __CPROVER_assume(y > x);
+
+  // This is always != 0, but symex doesn't know that.
+  // So, we force it to produce a case split on shadow memory access.
+  int choice = y / x;
+
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+
+  struct STRUCTNAME a;
+  a.next = (struct STRUCTNAME *)0;
+
+  assert(__CPROVER_get_field(&a, "field1") == 0);
+  assert(__CPROVER_get_field(&(a.data), "field1") == 0);
+  assert(__CPROVER_get_field(&(a.next), "field1") == 0);
+
+  __CPROVER_set_field(&(a.data), "field1", 1);
+  __CPROVER_set_field(&(a.next), "field1", 1);
+
+  assert(__CPROVER_get_field(&a, "field1") == 1);
+  assert(__CPROVER_get_field(&(a.data), "field1") == 1);
+  assert(__CPROVER_get_field(&(a.next), "field1") == 1);
+
+  struct STRUCTNAME b;
+  b.next = (struct STRUCTNAME *)0;
+  if(choice)
+  {
+    a.next = &b;
+  }
+
+  assert(__CPROVER_get_field(&a, "field1") == 1);
+  assert(__CPROVER_get_field(&(a.data), "field1") == 1);
+  assert(__CPROVER_get_field(&(a.next), "field1") == 1);
+  // No warning here.
+  assert(__CPROVER_get_field(a.next, "field1") == 0);
+
+  // No warning here.
+  __CPROVER_set_field(&((*(a.next)).data), "field1", 1);
+
+  // No warning here.
+  assert(__CPROVER_get_field(a.next, "field1") == 1);
+
+  struct STRUCTNAME c;
+  c.next = (struct STRUCTNAME *)0;
+  if(choice)
+  {
+    b.next = &c;
+  }
+
+  // No warning here.
+  assert(__CPROVER_get_field((*(a.next)).next, "field1") == 0);
+
+  // No warning here.
+  __CPROVER_set_field(&((*(*(a.next)).next).data), "field1", 1);
+
+  // No warning here.
+  assert(__CPROVER_get_field((*(a.next)).next, "field1") == 1);
+}

regression/cbmc-shadow-memory/linked-list2/test.desc

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