Add tests for shadow memory accessed via void pointers

Checks that accessing shadow memory through void pointers
returns the expected error messages, unless the correct
casts have been applied.

Author: peterschrammel

regression/cbmc-shadow-memory/void-ptr-param-get1/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct STRUCTNAME
+{
+  int x1;
+  int B1[3];
+};
+
+void f_void_ptr(void *s)
+{
+  assert(__CPROVER_get_field(s, "field1") == 0);
+}
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (char)0);
+
+  struct STRUCTNAME z;
+  f_void_ptr(&z);
+}

regression/cbmc-shadow-memory/void-ptr-param-get1/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+Shadow memory: cannot get shadow memory via type void\* for f_void_ptr::s
+--
+^warning: ignoring

regression/cbmc-shadow-memory/void-ptr-param-set1/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct STRUCTNAME
+{
+  int x1;
+  int B1[3];
+};
+
+void f_void_ptr(void *s)
+{
+  __CPROVER_set_field(s, "field1", 1);
+  assert(__CPROVER_get_field((struct STRUCTNAME *)s, "field1") == 1);
+}
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (char)0);
+
+  struct STRUCTNAME z;
+  f_void_ptr(&z);
+}

regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+Shadow memory: cannot set shadow memory via type void\* for f_void_ptr::s
+--
+^warning: ignoring

regression/cbmc-shadow-memory/void-ptr-param2/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct STRUCTNAME
+{
+  int x1;
+  int B1[3];
+};
+
+void f_void_ptr_cast(void *s)
+{
+  assert(__CPROVER_get_field((struct STRUCTNAME *)s, "field1") == 0);
+  __CPROVER_set_field(&((struct STRUCTNAME *)s)->x1, "field1", 1);
+  assert(__CPROVER_get_field((struct STRUCTNAME *)s, "field1") == 1);
+}
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (char)0);
+
+  struct STRUCTNAME z;
+  f_void_ptr_cast(&z);
+}

regression/cbmc-shadow-memory/void-ptr-param2/test.desc

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