diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
index d3a5ae972af..21a262a5ae5 100644
--- a/regression/CMakeLists.txt
+++ b/regression/CMakeLists.txt
@@ -38,6 +38,7 @@ add_subdirectory(cbmc-cover)
 add_subdirectory(cbmc-incr-oneloop)
 add_subdirectory(cbmc-incr-smt2)
 add_subdirectory(cbmc-incr)
+add_subdirectory(cbmc-shadow-memory)
 add_subdirectory(cbmc-output-file)
 add_subdirectory(cbmc-with-incr)
 add_subdirectory(array-refinement-with-incr)
diff --git a/regression/Makefile b/regression/Makefile
index dc734b936a4..1d1a28e0e7e 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -1,7 +1,8 @@
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are
 # listed with decreasing runtimes (i.e. longest running at the top)
-DIRS = cbmc \
+DIRS = cbmc-shadow-memory \
+       cbmc \
        cbmc-library \
        cprover \
        crangler \
diff --git a/regression/cbmc-shadow-memory/CMakeLists.txt b/regression/cbmc-shadow-memory/CMakeLists.txt
new file mode 100644
index 00000000000..93d5ee716c2
--- /dev/null
+++ b/regression/cbmc-shadow-memory/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/cbmc-shadow-memory/Makefile b/regression/cbmc-shadow-memory/Makefile
new file mode 100644
index 00000000000..d86a43477e6
--- /dev/null
+++ b/regression/cbmc-shadow-memory/Makefile
@@ -0,0 +1,22 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+
+test-cprover-smt2:
+	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.smt2' -execdir $(RM) '{}' \;
+	$(RM) tests.log
diff --git a/regression/cbmc-shadow-memory/char1/main.c b/regression/cbmc-shadow-memory/char1/main.c
new file mode 100644
index 00000000000..cdec0e8797f
--- /dev/null
+++ b/regression/cbmc-shadow-memory/char1/main.c
@@ -0,0 +1,59 @@
+#include <assert.h>
+
+// Add some string constants to confuse the value sets.
+const char *x1 = "This is a short string constant";
+const char *x2 = "This is a loooooooooooooonger string constant";
+const char *x3 = "And yet another string constant";
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+  __CPROVER_field_decl_global("field1", (_Bool)0);
+
+  // Add some string constants to confuse the value sets.
+  const char *y1 = "Yes, this is a short string constant";
+  const char *y2 = "Yes, this is a loooooooooooooonger string constant";
+  const char *y3 = "Yes, and yet another string constant";
+
+  char *a;
+  assert(__CPROVER_get_field(a, "field1") == 0);
+  assert(__CPROVER_get_field(&a, "field1") == 0);
+  // Cannot set because a doesn't point anywhere.
+  __CPROVER_set_field(a, "field1", 1);
+  // Hence, the value is still 0.
+  assert(__CPROVER_get_field(a, "field1") == 0);
+  assert(__CPROVER_get_field(&a, "field1") == 0);
+
+  __CPROVER_set_field(a, "field1", 0);
+  __CPROVER_set_field(&a, "field1", 1);
+  assert(__CPROVER_get_field(a, "field1") == 0);
+  assert(__CPROVER_get_field(&a, "field1") == 1);
+
+  char *b = (char *)0;
+  assert(__CPROVER_get_field(b, "field1") == 0);
+  assert(__CPROVER_get_field(&b, "field1") == 0);
+  // Cannot set because b points to NULL.
+  __CPROVER_set_field(b, "field1", 1);
+  // Hence, the value is still 0.
+  assert(__CPROVER_get_field(b, "field1") == 0);
+  assert(__CPROVER_get_field(&b, "field1") == 0);
+
+  __CPROVER_set_field(b, "field1", 0);
+  __CPROVER_set_field(&b, "field1", 1);
+  assert(__CPROVER_get_field(b, "field1") == 0);
+  assert(__CPROVER_get_field(&b, "field1") == 1);
+
+  static char *c;
+  assert(__CPROVER_get_field(c, "field1") == 0);
+  assert(__CPROVER_get_field(&c, "field1") == 0);
+  // Cannot set because c doesn't point anywhere.
+  __CPROVER_set_field(c, "field1", 1);
+  // Hence, the value is still 0.
+  assert(__CPROVER_get_field(c, "field1") == 0);
+  assert(__CPROVER_get_field(&c, "field1") == 0);
+
+  __CPROVER_set_field(c, "field1", 0);
+  __CPROVER_set_field(&c, "field1", 1);
+  assert(__CPROVER_get_field(c, "field1") == 0);
+  assert(__CPROVER_get_field(&c, "field1") == 1);
+}
diff --git a/regression/cbmc-shadow-memory/char1/test.desc b/regression/cbmc-shadow-memory/char1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/char1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/constchar-param1/main.c b/regression/cbmc-shadow-memory/constchar-param1/main.c
new file mode 100644
index 00000000000..3acc3889914
--- /dev/null
+++ b/regression/cbmc-shadow-memory/constchar-param1/main.c
@@ -0,0 +1,53 @@
+#include <assert.h>
+
+void test(const char *str)
+{
+  // Set shadow memory for some characters
+  for(int i = 1; i < 6; ++i)
+  {
+    __CPROVER_set_field(&str[i], "field1", 1);
+  }
+
+  // Copy string constant into buffer
+  char buffer[10];
+  for(int i = 0; i < 7; ++i)
+  {
+    buffer[i] = str[i];
+    __CPROVER_set_field(
+      &buffer[i], "field1", __CPROVER_get_field(&str[i], "field1"));
+  }
+
+  // Check that shadow memory has not been copied
+  for(int i = 0; i < 7; ++i)
+  {
+    assert(__CPROVER_get_field(&buffer[0], "field1") == 0);
+  }
+
+  // Copy shadow memory
+  for(int i = 0; i < 7; ++i)
+  {
+    __CPROVER_set_field(
+      &buffer[i], "field1", __CPROVER_get_field(&str[i], "field1"));
+  }
+
+  // Check that shadow memory has been copied
+  assert(__CPROVER_get_field(&buffer[0], "field1") == 0);
+  assert(__CPROVER_get_field(&buffer[1], "field1") == 1);
+  assert(__CPROVER_get_field(&buffer[2], "field1") == 1);
+  assert(__CPROVER_get_field(&buffer[3], "field1") == 1);
+  assert(__CPROVER_get_field(&buffer[4], "field1") == 1);
+  assert(__CPROVER_get_field(&buffer[5], "field1") == 1);
+  assert(__CPROVER_get_field(&buffer[6], "field1") == 0);
+  assert(__CPROVER_get_field(&buffer[7], "field1") == 0);
+  assert(__CPROVER_get_field(&buffer[8], "field1") == 0);
+  assert(__CPROVER_get_field(&buffer[9], "field1") == 0);
+}
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+  // Needed because the string constant is in the global pool.
+  __CPROVER_field_decl_global("field1", (_Bool)0);
+
+  test("!Hello!");
+}
diff --git a/regression/cbmc-shadow-memory/constchar-param1/test.desc b/regression/cbmc-shadow-memory/constchar-param1/test.desc
new file mode 100644
index 00000000000..482449453e2
--- /dev/null
+++ b/regression/cbmc-shadow-memory/constchar-param1/test.desc
@@ -0,0 +1,9 @@
+FUTURE
+main.c
+--unwind 11
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^Generated 11 VCC\(s\), 0 remaining after simplification$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/constchar-pointers1/main.c b/regression/cbmc-shadow-memory/constchar-pointers1/main.c
new file mode 100644
index 00000000000..c37098c36b1
--- /dev/null
+++ b/regression/cbmc-shadow-memory/constchar-pointers1/main.c
@@ -0,0 +1,36 @@
+#include <assert.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+  // Needed because the string constant is in the global pool.
+  __CPROVER_field_decl_global("field1", (_Bool)0);
+
+  const char *str = "!Hello!";
+
+  // Set shadow memory for some characters
+  for(int i = 1; i < 6; ++i)
+  {
+    __CPROVER_set_field(&str[i], "field1", 1);
+  }
+
+  // Populate with pointers into string constant
+  char *pointers[10];
+  for(int i = 0; i < 7; ++i)
+  {
+    pointers[i] = &str[i];
+  }
+
+  // Check that we can read the string constant's shadow memory
+  // through the pointers.
+  assert(__CPROVER_get_field(pointers[0], "field1") == 0);
+  assert(__CPROVER_get_field(pointers[1], "field1") == 1);
+  assert(__CPROVER_get_field(pointers[2], "field1") == 1);
+  assert(__CPROVER_get_field(pointers[3], "field1") == 1);
+  assert(__CPROVER_get_field(pointers[4], "field1") == 1);
+  assert(__CPROVER_get_field(pointers[5], "field1") == 1);
+  assert(__CPROVER_get_field(pointers[6], "field1") == 0);
+  assert(__CPROVER_get_field(pointers[7], "field1") == 0);
+  assert(__CPROVER_get_field(pointers[8], "field1") == 0);
+  assert(__CPROVER_get_field(pointers[9], "field1") == 0);
+}
diff --git a/regression/cbmc-shadow-memory/constchar-pointers1/test.desc b/regression/cbmc-shadow-memory/constchar-pointers1/test.desc
new file mode 100644
index 00000000000..f3ae1d03751
--- /dev/null
+++ b/regression/cbmc-shadow-memory/constchar-pointers1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+--unwind 11
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/custom-init1/main.c b/regression/cbmc-shadow-memory/custom-init1/main.c
new file mode 100644
index 00000000000..ab919f2fd56
--- /dev/null
+++ b/regression/cbmc-shadow-memory/custom-init1/main.c
@@ -0,0 +1,95 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct STRUCTNAME
+{
+  int x1;
+  int B1[3];
+};
+
+// Test initialization of various data types with custom values
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)1);
+  __CPROVER_field_decl_local("field2", (unsigned __CPROVER_bitvector[6])33);
+  __CPROVER_field_decl_global("field1", (_Bool)1);
+  __CPROVER_field_decl_global("field2", (unsigned __CPROVER_bitvector[6])33);
+
+  int y;
+  assert(__CPROVER_get_field(&y, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&y) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&y) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&y) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&y, "field1") == 1);
+  assert(__CPROVER_get_field(&y, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&y) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&y) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&y) + 3, "field2") == 33);
+
+  int A[5];
+  assert(__CPROVER_get_field(&A[2], "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&A[2], "field1") == 1);
+  assert(__CPROVER_get_field(&A[2], "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 3, "field2") == 33);
+
+  struct STRUCTNAME m;
+  assert(__CPROVER_get_field(&m.B1[1], "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&m.B1[1], "field1") == 1);
+  assert(__CPROVER_get_field(&m.B1[1], "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 3, "field2") == 33);
+
+  struct STRUCTNAME n[3];
+  assert(__CPROVER_get_field(&n[2].x1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&n[2].x1, "field1") == 1);
+  assert(__CPROVER_get_field(&n[2].x1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 3, "field2") == 33);
+
+  short *z = malloc(10 * sizeof(short));
+  assert(__CPROVER_get_field(&z[7], "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&z[7]) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(&z[7], "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&z[7]) + 1, "field2") == 33);
+
+  struct STRUCTNAME *p = malloc(sizeof(struct STRUCTNAME));
+  assert(__CPROVER_get_field(&p->B1[1], "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&p->B1[1], "field1") == 1);
+  assert(__CPROVER_get_field(&p->B1[1], "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 3, "field2") == 33);
+
+  struct STRUCTNAME *u = malloc(3 * sizeof(struct STRUCTNAME));
+  assert(__CPROVER_get_field(&u[2].x1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&u[2].x1, "field1") == 1);
+  assert(__CPROVER_get_field(&u[2].x1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 3, "field2") == 33);
+
+  const char *w = "A string constant";
+  assert(__CPROVER_get_field(&w[0], "field1") == 1);
+  assert(__CPROVER_get_field(&w[5], "field1") == 1);
+  assert(__CPROVER_get_field(&w[0], "field2") == 33);
+  assert(__CPROVER_get_field(&w[5], "field2") == 33);
+}
diff --git a/regression/cbmc-shadow-memory/custom-init1/test.desc b/regression/cbmc-shadow-memory/custom-init1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/custom-init1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/errno1/main.c b/regression/cbmc-shadow-memory/errno1/main.c
new file mode 100644
index 00000000000..3ea036d804c
--- /dev/null
+++ b/regression/cbmc-shadow-memory/errno1/main.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <errno.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+  __CPROVER_field_decl_global("field1", (_Bool)0);
+
+  int *error = __errno();
+
+  assert(__CPROVER_get_field(error, "field1") == 0);
+
+  __CPROVER_set_field(error, "field1", 1);
+  assert(__CPROVER_get_field(error, "field1") == 1);
+}
diff --git a/regression/cbmc-shadow-memory/errno1/test.desc b/regression/cbmc-shadow-memory/errno1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/errno1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/float1/main.c b/regression/cbmc-shadow-memory/float1/main.c
new file mode 100644
index 00000000000..c7b3055b8bc
--- /dev/null
+++ b/regression/cbmc-shadow-memory/float1/main.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (unsigned __CPROVER_bitvector[7])0);
+
+  float x;
+
+  // Check that shadow memory has been initialized to zero.
+  assert(!__CPROVER_get_field(&x, "field1"));
+
+  // Check that shadow memory has been set to the chosen
+  // nondeterministic value.
+  unsigned __CPROVER_bitvector[7] v;
+  __CPROVER_set_field(&x, "field1", v);
+  assert(__CPROVER_get_field(&x, "field1") == v);
+}
diff --git a/regression/cbmc-shadow-memory/float1/test.desc b/regression/cbmc-shadow-memory/float1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/float1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/getenv1/main.c b/regression/cbmc-shadow-memory/getenv1/main.c
new file mode 100644
index 00000000000..5e8163ea504
--- /dev/null
+++ b/regression/cbmc-shadow-memory/getenv1/main.c
@@ -0,0 +1,13 @@
+#include <stdlib.h>
+
+void main()
+{
+  __CPROVER_field_decl_global("dr_write", (_Bool)0);
+
+  char *env = getenv("PATH");
+  __CPROVER_assume(env != NULL);
+  assert(!__CPROVER_get_field(env, "dr_write"));
+
+  __CPROVER_set_field(env, "dr_write", 1);
+  assert(__CPROVER_get_field(env, "dr_write"));
+}
diff --git a/regression/cbmc-shadow-memory/getenv1/test.desc b/regression/cbmc-shadow-memory/getenv1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/getenv1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/global1/main.c b/regression/cbmc-shadow-memory/global1/main.c
new file mode 100644
index 00000000000..33c9f79dc19
--- /dev/null
+++ b/regression/cbmc-shadow-memory/global1/main.c
@@ -0,0 +1,261 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct STRUCTNAME
+{
+  int x1;
+  int B1[3];
+};
+
+int y;
+int *z;
+int **w;
+struct STRUCTNAME m, *p;
+int A[5];
+struct STRUCTNAME n[3];
+
+void scalars_and_pointers_to_scalars()
+{
+  y = 10;
+
+  assert(__CPROVER_get_field(&y, "field1") == 0);
+  assert(__CPROVER_get_field(&y, "field2") == 0);
+
+  assert(__CPROVER_get_field(&z, "field1") == 0);
+  assert(__CPROVER_get_field(&z, "field2") == 0);
+
+  __CPROVER_set_field(&y, "field1", 3);
+  __CPROVER_set_field(&y, "field2", 4);
+  __CPROVER_set_field(&z, "field1", 5);
+  __CPROVER_set_field(&z, "field2", 6);
+
+  z = &y;
+
+  assert(__CPROVER_get_field(z, "field1") == 3);
+  assert(__CPROVER_get_field(z, "field2") == 4);
+
+  assert(__CPROVER_get_field(&z, "field1") == 5);
+  assert(__CPROVER_get_field(&z, "field2") == 6);
+
+  assert(__CPROVER_get_field(z, "field1") == __CPROVER_get_field(&y, "field1"));
+  assert(__CPROVER_get_field(z, "field2") == __CPROVER_get_field(&y, "field2"));
+
+  w = &z;
+
+  assert(__CPROVER_get_field(&w, "field1") == 0);
+  assert(__CPROVER_get_field(&w, "field2") == 0);
+
+  assert(__CPROVER_get_field(w, "field1") == 5);
+  assert(__CPROVER_get_field(w, "field2") == 6);
+
+  assert(__CPROVER_get_field(*w, "field1") == 3);
+  assert(__CPROVER_get_field(*w, "field2") == 4);
+}
+
+void arrays_and_pointers_into_arrays()
+{
+  z = &(A[4]);
+
+  assert(__CPROVER_get_field(z, "field1") == 0);
+  assert(__CPROVER_get_field(z, "field2") == 0);
+
+  __CPROVER_set_field(&(A[3]), "field1", 13);
+  __CPROVER_set_field(&(A[3]), "field2", 14);
+  __CPROVER_set_field(z, "field1", 15);
+  __CPROVER_set_field(z, "field2", 16);
+
+  z = A;
+
+  assert(__CPROVER_get_field(z + 3, "field1") == 13);
+  assert(__CPROVER_get_field(z + 3, "field2") == 14);
+  assert(__CPROVER_get_field(z + 4, "field1") == 15);
+  assert(__CPROVER_get_field(z + 4, "field2") == 16);
+
+  int i;
+  __CPROVER_assume(0 <= i && i < 5);
+  __CPROVER_set_field(&(A[i]), "field1", 42);
+  assert(__CPROVER_get_field(&(A[i]), "field1") == 42);
+
+  z = &(A[i]);
+  __CPROVER_set_field(z, "field1", 43);
+  assert(__CPROVER_get_field(z, "field1") == 43);
+}
+
+void dynamically_allocated_arrays()
+{
+  z = malloc(10 * sizeof(int));
+
+  assert(__CPROVER_get_field(z, "field1") == 0);
+  assert(__CPROVER_get_field(z, "field2") == 0);
+
+  __CPROVER_set_field(&(z[3]), "field1", 13);
+  __CPROVER_set_field(&(z[3]), "field2", 14);
+  __CPROVER_set_field(z + 4, "field1", 15);
+  __CPROVER_set_field(z + 4, "field2", 16);
+
+  z += 3;
+
+  assert(__CPROVER_get_field(z, "field1") == 13);
+  assert(__CPROVER_get_field(z, "field2") == 14);
+  assert(__CPROVER_get_field(&(z[1]), "field1") == 15);
+  assert(__CPROVER_get_field(&(z[1]), "field2") == 16);
+
+  z -= 3;
+
+  int j;
+  __CPROVER_assume(0 <= j && j < 10);
+  __CPROVER_set_field(&(z[j]), "field1", 42);
+  assert(__CPROVER_get_field(&(z[j]), "field1") == 42);
+
+  z = &(z[j]);
+  __CPROVER_set_field(z, "field1", 43);
+  assert(__CPROVER_get_field(z, "field1") == 43);
+}
+
+void structs_and_pointers_into_structs()
+{
+  p = &m;
+
+  assert(__CPROVER_get_field(&(p->x1), "field1") == 0);
+  assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 0);
+
+  __CPROVER_set_field(&((*p).x1), "field1", 2);
+  __CPROVER_set_field(&((*p).B1[1]), "field2", 2);
+
+  assert(__CPROVER_get_field(&(p->x1), "field1") == 2);
+  assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 2);
+  assert(__CPROVER_get_field(&(p->B1[2]), "field1") == 0);
+
+  int *q = &(m.B1[2]);
+  assert(__CPROVER_get_field(q, "field1") == 0);
+  __CPROVER_set_field(q, "field1", 7);
+  assert(__CPROVER_get_field(q, "field1") == 7);
+
+  int l;
+  __CPROVER_assume(0 <= l && l < 3);
+  __CPROVER_set_field(&(m.B1[l]), "field1", 44);
+  assert(__CPROVER_get_field(&(m.B1[l]), "field1") == 44);
+
+  z = &(m.B1[l]);
+  __CPROVER_set_field(z, "field1", 45);
+  assert(__CPROVER_get_field(z, "field1") == 45);
+}
+
+void dynamically_allocated_structs()
+{
+  p = malloc(sizeof(struct STRUCTNAME));
+
+  assert(__CPROVER_get_field(&(p->x1), "field1") == 0);
+  assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 0);
+
+  __CPROVER_set_field(&((*p).x1), "field1", 2);
+  __CPROVER_set_field(&((*p).B1[1]), "field2", 2);
+
+  assert(__CPROVER_get_field(&(p->x1), "field1") == 2);
+  assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 2);
+  assert(__CPROVER_get_field(&(p->B1[2]), "field1") == 0);
+
+  q = &(p->B1[2]);
+  assert(__CPROVER_get_field(q, "field1") == 0);
+  __CPROVER_set_field(q, "field1", 7);
+  assert(__CPROVER_get_field(q, "field1") == 7);
+
+  int k;
+  __CPROVER_assume(0 <= k && k < 3);
+  __CPROVER_set_field(&(p->B1[k]), "field1", 44);
+  assert(__CPROVER_get_field(&(p->B1[k]), "field1") == 44);
+
+  z = &(p->B1[k]);
+  __CPROVER_set_field(z, "field1", 45);
+  assert(__CPROVER_get_field(z, "field1") == 45);
+}
+
+void arrays_of_structs_and_pointers_into_them()
+{
+  assert(__CPROVER_get_field(&(n[1].x1), "field1") == 0);
+  assert(__CPROVER_get_field(&(n[1].B1[1]), "field2") == 0);
+
+  p = &(n[2]);
+
+  __CPROVER_set_field(&(n[1].x1), "field1", 1);
+  __CPROVER_set_field(&(p->x1), "field1", 2);
+  assert(__CPROVER_get_field(&(n[1].x1), "field1") == 1);
+  assert(__CPROVER_get_field(&(p->x1), "field1") == 2);
+
+  __CPROVER_set_field(&(n[1].B1[1]), "field2", 3);
+  __CPROVER_set_field(&(p->B1[1]), "field2", 4);
+  assert(__CPROVER_get_field(&(n[1].B1[1]), "field2") == 3);
+  assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 4);
+
+  q = &(n[1].x1);
+  assert(__CPROVER_get_field(q, "field1") == 1);
+  __CPROVER_set_field(q, "field1", 5);
+  assert(__CPROVER_get_field(q, "field1") == 5);
+
+  q = &(n[1].B1[1]);
+  assert(__CPROVER_get_field(q, "field2") == 3);
+  __CPROVER_set_field(q, "field2", 6);
+  assert(__CPROVER_get_field(q, "field2") == 6);
+
+  int x;
+  __CPROVER_assume(0 <= x && x < 3);
+  __CPROVER_set_field(&(n[k].B1[x]), "field1", 46);
+  assert(__CPROVER_get_field(&(n[k].B1[x]), "field1") == 46);
+
+  z = &(n[k].B1[x]);
+  __CPROVER_set_field(z, "field1", 47);
+  assert(__CPROVER_get_field(z, "field1") == 47);
+}
+
+void dynamically_allocated_arrays_of_structs()
+{
+  struct STRUCTNAME *u = malloc(3 * sizeof(struct STRUCTNAME));
+
+  assert(__CPROVER_get_field(&(u[1].x1), "field1") == 0);
+  assert(__CPROVER_get_field(&(u[1].B1[1]), "field2") == 0);
+
+  p = &(u[2]);
+
+  __CPROVER_set_field(&(u[1].x1), "field1", 1);
+  __CPROVER_set_field(&(p->x1), "field1", 2);
+  assert(__CPROVER_get_field(&(u[1].x1), "field1") == 1);
+  assert(__CPROVER_get_field(&(p->x1), "field1") == 2);
+
+  __CPROVER_set_field(&(u[1].B1[1]), "field2", 3);
+  __CPROVER_set_field(&(p->B1[1]), "field2", 4);
+  assert(__CPROVER_get_field(&(u[1].B1[1]), "field2") == 3);
+  assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 4);
+
+  q = &(u[1].x1);
+  assert(__CPROVER_get_field(q, "field1") == 1);
+  __CPROVER_set_field(q, "field1", 5);
+  assert(__CPROVER_get_field(q, "field1") == 5);
+
+  q = &(u[1].B1[1]);
+  assert(__CPROVER_get_field(q, "field2") == 3);
+  __CPROVER_set_field(q, "field2", 6);
+  assert(__CPROVER_get_field(q, "field2") == 6);
+
+  int t;
+  __CPROVER_assume(0 <= t && t < 3);
+  __CPROVER_set_field(&(u[k].B1[t]), "field1", 46);
+  assert(__CPROVER_get_field(&(u[k].B1[t]), "field1") == 46);
+
+  z = &(u[k].B1[t]);
+  __CPROVER_set_field(z, "field1", 47);
+  assert(__CPROVER_get_field(z, "field1") == 47);
+}
+
+int main()
+{
+  __CPROVER_field_decl_global("field1", (char)0);
+  __CPROVER_field_decl_global("field2", (__CPROVER_bitvector[6])0);
+
+  scalars_and_pointers_to_scalars();
+  arrays_and_pointers_into_arrays();
+  dynamically_allocated_arrays();
+  structs_and_pointers_into_structs();
+  dynamically_allocated_structs();
+  arrays_of_structs_and_pointers_into_them();
+  dynamically_allocated_arrays_of_structs();
+}
diff --git a/regression/cbmc-shadow-memory/global1/test.desc b/regression/cbmc-shadow-memory/global1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/global1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/linked-list1/main.c b/regression/cbmc-shadow-memory/linked-list1/main.c
new file mode 100644
index 00000000000..ae9a75bd5e8
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc-shadow-memory/linked-list1/test.desc b/regression/cbmc-shadow-memory/linked-list1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/linked-list1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/linked-list2/main.c b/regression/cbmc-shadow-memory/linked-list2/main.c
new file mode 100644
index 00000000000..3bb1a723dab
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc-shadow-memory/linked-list2/test.desc b/regression/cbmc-shadow-memory/linked-list2/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/linked-list2/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/local1/main.c b/regression/cbmc-shadow-memory/local1/main.c
new file mode 100644
index 00000000000..749e4da442c
--- /dev/null
+++ b/regression/cbmc-shadow-memory/local1/main.c
@@ -0,0 +1,167 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct STRUCTNAME
+{
+  int x1;
+  int B1[3];
+};
+
+void scalars_and_pointers_to_scalars()
+{
+  int y = 10;
+
+  assert(__CPROVER_get_field(&y, "field1") == 0);
+  assert(__CPROVER_get_field(&y, "field2") == 0);
+
+  int *z;
+
+  assert(__CPROVER_get_field(&z, "field1") == 0);
+  assert(__CPROVER_get_field(&z, "field2") == 0);
+
+  __CPROVER_set_field(&y, "field1", 3);
+  __CPROVER_set_field(&y, "field2", 4);
+  __CPROVER_set_field(&z, "field1", 5);
+  __CPROVER_set_field(&z, "field2", 6);
+
+  z = &y;
+
+  assert(__CPROVER_get_field(z, "field1") == 3);
+  assert(__CPROVER_get_field(z, "field2") == 4);
+
+  assert(__CPROVER_get_field(&z, "field1") == 5);
+  assert(__CPROVER_get_field(&z, "field2") == 6);
+
+  assert(__CPROVER_get_field(z, "field1") == __CPROVER_get_field(&y, "field1"));
+  assert(__CPROVER_get_field(z, "field2") == __CPROVER_get_field(&y, "field2"));
+
+  int **w;
+
+  w = &z;
+
+  assert(__CPROVER_get_field(&w, "field1") == 0);
+  assert(__CPROVER_get_field(&w, "field2") == 0);
+
+  assert(__CPROVER_get_field(w, "field1") == 5);
+  assert(__CPROVER_get_field(w, "field2") == 6);
+
+  assert(__CPROVER_get_field(*w, "field1") == 3);
+  assert(__CPROVER_get_field(*w, "field2") == 4);
+}
+
+void arrays_and_pointers_into_arrays()
+{
+  int A[5];
+
+  z = &(A[4]);
+
+  assert(__CPROVER_get_field(z, "field1") == 0);
+  assert(__CPROVER_get_field(z, "field2") == 0);
+
+  __CPROVER_set_field(&(A[3]), "field1", 13);
+  __CPROVER_set_field(&(A[3]), "field2", 14);
+  __CPROVER_set_field(z, "field1", 15);
+  __CPROVER_set_field(z, "field2", 16);
+
+  z = A;
+
+  assert(__CPROVER_get_field(z + 3, "field1") == 13);
+  assert(__CPROVER_get_field(z + 3, "field2") == 14);
+  assert(__CPROVER_get_field(z + 4, "field1") == 15);
+  assert(__CPROVER_get_field(z + 4, "field2") == 16);
+
+  int i;
+  __CPROVER_assume(0 <= i && i < 5);
+  __CPROVER_set_field(&(A[i]), "field1", 42);
+  assert(__CPROVER_get_field(&(A[i]), "field1") == 42);
+
+  z = &(A[i]);
+  __CPROVER_set_field(z, "field1", 43);
+  assert(__CPROVER_get_field(z, "field1") == 43);
+}
+
+void structs_and_pointers_into_structs()
+{
+  struct STRUCTNAME m;
+  struct STRUCTNAME *p;
+
+  assert(__CPROVER_get_field(&p, "field1") == 0);
+  __CPROVER_set_field(&p, "field1", 1);
+  assert(__CPROVER_get_field(&p, "field1") == 1);
+
+  p = &m;
+
+  assert(__CPROVER_get_field(&(p->x1), "field1") == 0);
+  assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 0);
+
+  __CPROVER_set_field(&((*p).x1), "field1", 2);
+  __CPROVER_set_field(&((*p).B1[1]), "field2", 2);
+
+  assert(__CPROVER_get_field(&(p->x1), "field1") == 2);
+  assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 2);
+  assert(__CPROVER_get_field(&(p->B1[2]), "field1") == 0);
+
+  int *q = &(m.B1[2]);
+  assert(__CPROVER_get_field(q, "field1") == 0);
+  __CPROVER_set_field(q, "field1", 7);
+  assert(__CPROVER_get_field(q, "field1") == 7);
+
+  int j;
+  __CPROVER_assume(0 <= j && j < 3);
+  __CPROVER_set_field(&(m.B1[j]), "field1", 44);
+  assert(__CPROVER_get_field(&(m.B1[j]), "field1") == 44);
+
+  z = &(m.B1[j]);
+  __CPROVER_set_field(z, "field1", 45);
+  assert(__CPROVER_get_field(z, "field1") == 45);
+}
+
+void arrays_of_structs_and_pointers_into_them()
+{
+  struct STRUCTNAME n[3];
+
+  assert(__CPROVER_get_field(&(n[1].x1), "field1") == 0);
+  assert(__CPROVER_get_field(&(n[1].B1[1]), "field2") == 0);
+
+  p = &(n[2]);
+
+  __CPROVER_set_field(&(n[1].x1), "field1", 1);
+  __CPROVER_set_field(&(p->x1), "field1", 2);
+  assert(__CPROVER_get_field(&(n[1].x1), "field1") == 1);
+  assert(__CPROVER_get_field(&(p->x1), "field1") == 2);
+
+  __CPROVER_set_field(&(n[1].B1[1]), "field2", 3);
+  __CPROVER_set_field(&(p->B1[1]), "field2", 4);
+  assert(__CPROVER_get_field(&(n[1].B1[1]), "field2") == 3);
+  assert(__CPROVER_get_field(&(p->B1[1]), "field2") == 4);
+
+  q = &(n[1].x1);
+  assert(__CPROVER_get_field(q, "field1") == 1);
+  __CPROVER_set_field(q, "field1", 5);
+  assert(__CPROVER_get_field(q, "field1") == 5);
+
+  q = &(n[1].B1[1]);
+  assert(__CPROVER_get_field(q, "field2") == 3);
+  __CPROVER_set_field(q, "field2", 6);
+  assert(__CPROVER_get_field(q, "field2") == 6);
+
+  int k;
+  __CPROVER_assume(0 <= k && k < 3);
+  __CPROVER_set_field(&(n[k].B1[j]), "field1", 46);
+  assert(__CPROVER_get_field(&(n[k].B1[j]), "field1") == 46);
+
+  z = &(n[k].B1[j]);
+  __CPROVER_set_field(z, "field1", 47);
+  assert(__CPROVER_get_field(z, "field1") == 47);
+}
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (char)0);
+  __CPROVER_field_decl_local("field2", (__CPROVER_bitvector[6])0);
+
+  scalars_and_pointers_to_scalars();
+  arrays_and_pointers_into_arrays();
+  structs_and_pointers_into_structs();
+  arrays_of_structs_and_pointers_into_them();
+}
diff --git a/regression/cbmc-shadow-memory/local1/test.desc b/regression/cbmc-shadow-memory/local1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/local1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/malloc1/main.c b/regression/cbmc-shadow-memory/malloc1/main.c
new file mode 100644
index 00000000000..253ce431c3b
--- /dev/null
+++ b/regression/cbmc-shadow-memory/malloc1/main.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdlib.h>
+
+extern int nondet_int();
+
+void main()
+{
+  __CPROVER_field_decl_global("field", (unsigned __CPROVER_bitvector[2])0);
+
+  char *x = (char *)malloc((sizeof(char)) * 5l);
+
+  assert(__CPROVER_get_field(x, "field") == 0);
+  assert(__CPROVER_get_field(x + 1, "field") == 0);
+
+  __CPROVER_set_field(x + 1, "field", 1);
+
+  assert(__CPROVER_get_field(x, "field") == 0);
+  assert(__CPROVER_get_field(x + 1, "field") == 1);
+}
diff --git a/regression/cbmc-shadow-memory/malloc1/test.desc b/regression/cbmc-shadow-memory/malloc1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/malloc1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/maybe-null1/main.c b/regression/cbmc-shadow-memory/maybe-null1/main.c
new file mode 100644
index 00000000000..a81b15ac822
--- /dev/null
+++ b/regression/cbmc-shadow-memory/maybe-null1/main.c
@@ -0,0 +1,30 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)1);
+  int x;
+  int *y = NULL;
+  int c;
+  int *z;
+
+  // Goto-symex is expected to create a case split for dereferencing z.
+  __CPROVER_assume(c > 0);
+  if(c)
+    z = &x;
+  else
+    z = y;
+
+  // Check initialization
+  assert(__CPROVER_get_field(z, "field1") == 1);
+
+  // z actually points to x, which has valid shadow memory.
+  __CPROVER_set_field(z, "field1", 0);
+  assert(__CPROVER_get_field(z, "field1") == 0);
+  assert(__CPROVER_get_field(&x, "field1") == 0);
+
+  // y is NULL, which has no valid shadow memory
+  // and thus returns the default value.
+  assert(__CPROVER_get_field(y, "field1") == 1);
+}
diff --git a/regression/cbmc-shadow-memory/maybe-null1/test.desc b/regression/cbmc-shadow-memory/maybe-null1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/maybe-null1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/memcpy1/main.c b/regression/cbmc-shadow-memory/memcpy1/main.c
new file mode 100644
index 00000000000..9e2526ba2db
--- /dev/null
+++ b/regression/cbmc-shadow-memory/memcpy1/main.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <string.h>
+
+int src[10];
+
+int main()
+{
+  __CPROVER_field_decl_local("field", (_Bool)0);
+  __CPROVER_field_decl_global("field", (_Bool)0);
+
+  assert(src[9] == 0);
+  assert(__CPROVER_get_field(&(src[9]), "field") == 0);
+
+  int dest[10];
+  dest[9] = 1;
+  assert(__CPROVER_get_field(&(dest[9]), "field") == 0);
+  __CPROVER_set_field(&(dest[9]), "field", 1);
+  assert(__CPROVER_get_field(&(dest[9]), "field") == 1);
+
+  memcpy(dest, src, 10 * sizeof(int));
+  assert(dest[9] == 0);
+  assert(__CPROVER_get_field(&(src[9]), "field") == 0);
+  assert(__CPROVER_get_field(&(dest[9]), "field") == 1);
+}
diff --git a/regression/cbmc-shadow-memory/memcpy1/test.desc b/regression/cbmc-shadow-memory/memcpy1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/memcpy1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/no-shadow-memory-matching1/main.c b/regression/cbmc-shadow-memory/no-shadow-memory-matching1/main.c
new file mode 100644
index 00000000000..0f8c68111b4
--- /dev/null
+++ b/regression/cbmc-shadow-memory/no-shadow-memory-matching1/main.c
@@ -0,0 +1,28 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct STRUCTNAME
+{
+  int x;
+};
+
+void f_charptr_val(char *__cs_param)
+{
+  // Access to shadow memory of z.
+  assert(__CPROVER_get_field(__cs_param, "field1") == 255);
+
+  // Fails because parameter itself doesn't have shadow memory.
+  assert(__CPROVER_get_field(&__cs_param, "field1") == 0);
+}
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (char)0);
+
+  char *__cs_threadargs[2];
+  struct STRUCTNAME z;
+  __CPROVER_set_field(&z, "field1", 255);
+
+  __cs_threadargs[1] = (char *)(&z);
+  f_charptr_val(__cs_threadargs[1]);
+}
diff --git a/regression/cbmc-shadow-memory/no-shadow-memory-matching1/test.desc b/regression/cbmc-shadow-memory/no-shadow-memory-matching1/test.desc
new file mode 100644
index 00000000000..0106ebceb8a
--- /dev/null
+++ b/regression/cbmc-shadow-memory/no-shadow-memory-matching1/test.desc
@@ -0,0 +1,9 @@
+FUTURE
+main.c
+--no-shadow-memory-matching '.*\.c:.*__cs_.*'
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^Shadow memory: field 'field1' expected to exist for
diff --git a/regression/cbmc-shadow-memory/nondet-pointer-into-struct1/main.c b/regression/cbmc-shadow-memory/nondet-pointer-into-struct1/main.c
new file mode 100644
index 00000000000..e90a32daf76
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc-shadow-memory/nondet-pointer-into-struct1/test.desc b/regression/cbmc-shadow-memory/nondet-pointer-into-struct1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/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
diff --git a/regression/cbmc-shadow-memory/nondet-size-arrays1/main.c b/regression/cbmc-shadow-memory/nondet-size-arrays1/main.c
new file mode 100644
index 00000000000..c462d2ff30d
--- /dev/null
+++ b/regression/cbmc-shadow-memory/nondet-size-arrays1/main.c
@@ -0,0 +1,108 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (char)0);
+  __CPROVER_field_decl_local("field2", (__CPROVER_bitvector[6])0);
+  __CPROVER_field_decl_global("field1", (char)0);
+  __CPROVER_field_decl_global("field2", (__CPROVER_bitvector[6])0);
+
+  /***********************
+   * Variable-size arrays
+   ***********************/
+
+  int n;
+  __CPROVER_assume(5 <= n && n < 10);
+  int A[n];
+
+  int *z = &(A[4]);
+
+  assert(__CPROVER_get_field(z, "field1") == 0);
+  assert(__CPROVER_get_field(z, "field2") == 0);
+
+  __CPROVER_set_field(&(A[3]), "field1", 13);
+  __CPROVER_set_field(&(A[3]), "field2", 14);
+  __CPROVER_set_field(z, "field1", 15);
+  __CPROVER_set_field(z, "field2", 16);
+
+  z = A;
+
+  assert(__CPROVER_get_field(z + 3, "field1") == 13);
+  assert(__CPROVER_get_field(z + 3, "field2") == 14);
+  assert(__CPROVER_get_field(z + 4, "field1") == 15);
+  assert(__CPROVER_get_field(z + 4, "field2") == 16);
+
+  int i;
+  __CPROVER_assume(0 <= i && i < n);
+  __CPROVER_set_field(&(A[i]), "field1", 42);
+  assert(__CPROVER_get_field(&(A[i]), "field1") == 42);
+
+  z = &(A[i]);
+  __CPROVER_set_field(z, "field1", 43);
+  assert(__CPROVER_get_field(z, "field1") == 43);
+
+  /***********************
+   * Variable-size arrays with malloc
+   ***********************/
+
+  int *B = malloc(n * sizeof(int));
+
+  z = &(B[4]);
+
+  assert(__CPROVER_get_field(z, "field1") == 0);
+  assert(__CPROVER_get_field(z, "field2") == 0);
+
+  __CPROVER_set_field(&(B[3]), "field1", 13);
+  __CPROVER_set_field(&(B[3]), "field2", 14);
+  __CPROVER_set_field(z, "field1", 15);
+  __CPROVER_set_field(z, "field2", 16);
+
+  z = B;
+
+  assert(__CPROVER_get_field(z + 3, "field1") == 13);
+  assert(__CPROVER_get_field(z + 3, "field2") == 14);
+  assert(__CPROVER_get_field(z + 4, "field1") == 15);
+  assert(__CPROVER_get_field(z + 4, "field2") == 16);
+
+  int i;
+  __CPROVER_assume(0 <= i && i < n);
+  __CPROVER_set_field(&(B[i]), "field1", 42);
+  assert(__CPROVER_get_field(&(B[i]), "field1") == 42);
+
+  z = &(B[i]);
+  __CPROVER_set_field(z, "field1", 43);
+  assert(__CPROVER_get_field(z, "field1") == 43);
+
+  /***********************
+   * Variable-size arrays with alloca
+   ***********************/
+
+  int *C = alloca(n * sizeof(int));
+
+  z = &(C[4]);
+
+  assert(__CPROVER_get_field(z, "field1") == 0);
+  assert(__CPROVER_get_field(z, "field2") == 0);
+
+  __CPROVER_set_field(&(C[3]), "field1", 13);
+  __CPROVER_set_field(&(C[3]), "field2", 14);
+  __CPROVER_set_field(z, "field1", 15);
+  __CPROVER_set_field(z, "field2", 16);
+
+  z = C;
+
+  assert(__CPROVER_get_field(z + 3, "field1") == 13);
+  assert(__CPROVER_get_field(z + 3, "field2") == 14);
+  assert(__CPROVER_get_field(z + 4, "field1") == 15);
+  assert(__CPROVER_get_field(z + 4, "field2") == 16);
+
+  int i;
+  __CPROVER_assume(0 <= i && i < n);
+  __CPROVER_set_field(&(C[i]), "field1", 42);
+  assert(__CPROVER_get_field(&(C[i]), "field1") == 42);
+
+  z = &(C[i]);
+  __CPROVER_set_field(z, "field1", 43);
+  assert(__CPROVER_get_field(z, "field1") == 43);
+}
diff --git a/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc b/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/param1/main.c b/regression/cbmc-shadow-memory/param1/main.c
new file mode 100644
index 00000000000..497c513f05e
--- /dev/null
+++ b/regression/cbmc-shadow-memory/param1/main.c
@@ -0,0 +1,128 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct STRUCTNAME
+{
+  int x1;
+  int B1[3];
+};
+
+void f_int_val(int x)
+{
+  // x has its own shadow memory
+  assert(__CPROVER_get_field(&x, "field1") == 0);
+  __CPROVER_set_field(&x, "field1", 1);
+  assert(__CPROVER_get_field(&x, "field1") == 1);
+}
+
+void f_intptr_ptr0(int *x)
+{
+  // we access the argument's shadow memory
+  assert(__CPROVER_get_field(x, "field1") == 255);
+  __CPROVER_set_field(x, "field1", 1);
+  assert(__CPROVER_get_field(x, "field1") == 1);
+}
+
+void f_intptr_ptr1(int *x)
+{
+  // we access the argument's shadow memory
+  assert(__CPROVER_get_field(x, "field1") == 1);
+  __CPROVER_set_field(x, "field1", 2);
+  assert(__CPROVER_get_field(x, "field1") == 2);
+}
+
+void f_intptr_val(int *x)
+{
+  // x has its own shadow memory
+  assert(__CPROVER_get_field(&x, "field1") == 0);
+  __CPROVER_set_field(&x, "field1", 3);
+  assert(__CPROVER_get_field(&x, "field1") == 3);
+}
+
+void f_intarray_ptr0(int x[])
+{
+  // we access the argument's shadow memory
+  assert(__CPROVER_get_field(&(x[0]), "field1") == 255);
+  __CPROVER_set_field(&(x[0]), "field1", 1);
+  assert(__CPROVER_get_field(&(x[0]), "field1") == 1);
+}
+
+void f_intarray_ptr1(int x[])
+{
+  // we access the argument's shadow memory
+  assert(__CPROVER_get_field(&(x[0]), "field1") == 1);
+  __CPROVER_set_field(&(x[0]), "field1", 2);
+  assert(__CPROVER_get_field(&(x[0]), "field1") == 2);
+}
+
+void f_struct_val(struct STRUCTNAME x)
+{
+  // x has its own shadow memory
+  assert(__CPROVER_get_field(&(x.B1[2]), "field1") == 0);
+  __CPROVER_set_field(&(x.B1[2]), "field1", 5);
+  assert(__CPROVER_get_field(&(x.B1[2]), "field1") == 5);
+}
+
+void f_structptr_ptr0(struct STRUCTNAME *x)
+{
+  // we access the argument's shadow memory
+  assert(__CPROVER_get_field(&(x->B1[2]), "field1") == 255);
+  __CPROVER_set_field(&(x->B1[2]), "field1", 1);
+  assert(__CPROVER_get_field(&(x->B1[2]), "field1") == 1);
+}
+
+void f_structptr_ptr1(struct STRUCTNAME *x)
+{
+  // we access the argument's shadow memory
+  assert(__CPROVER_get_field(&(x->B1[2]), "field1") == 1);
+  __CPROVER_set_field(&(x->B1[2]), "field1", 2);
+  assert(__CPROVER_get_field(&(x->B1[2]), "field1") == 2);
+}
+
+void f_structptr_val(struct STRUCTNAME *x)
+{
+  // x has its own shadow memory
+  assert(__CPROVER_get_field(&x, "field1") == 0);
+  __CPROVER_set_field(&x, "field1", 7);
+  assert(__CPROVER_get_field(&x, "field1") == 7);
+}
+
+void f_int_local(int rec, int value)
+{
+  // locals in each recursive call instance have their own shadow memory
+  int x;
+  assert(__CPROVER_get_field(&x, "field1") == 0);
+  __CPROVER_set_field(&x, "field1", value);
+  assert(__CPROVER_get_field(&x, "field1") == value);
+  if(rec)
+  {
+    f_int_local(0, value + 1);
+    assert(__CPROVER_get_field(&x, "field1") == value);
+  }
+}
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (char)0);
+  int x;
+  __CPROVER_set_field(&x, "field1", 255);
+  f_int_val(x);
+  f_int_val(x);
+  f_intptr_ptr0(&x);
+  f_intptr_ptr1(&x);
+  f_intptr_val(&x);
+  f_intptr_val(&x);
+  int y[1];
+  __CPROVER_set_field(&y[0], "field1", 255);
+  f_intarray_ptr0(y);
+  f_intarray_ptr1(y);
+  struct STRUCTNAME z;
+  __CPROVER_set_field(&z, "field1", 255);
+  f_struct_val(z);
+  f_struct_val(z);
+  f_structptr_ptr0(&z);
+  f_structptr_ptr1(&z);
+  f_structptr_val(&z);
+  f_structptr_val(&z);
+  f_int_local(1, 1);
+}
diff --git a/regression/cbmc-shadow-memory/param1/test.desc b/regression/cbmc-shadow-memory/param1/test.desc
new file mode 100644
index 00000000000..3ab59a8d649
--- /dev/null
+++ b/regression/cbmc-shadow-memory/param1/test.desc
@@ -0,0 +1,9 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^Shadow memory: cannot get_field for
diff --git a/regression/cbmc-shadow-memory/static1/main.c b/regression/cbmc-shadow-memory/static1/main.c
new file mode 100644
index 00000000000..49a620f58f3
--- /dev/null
+++ b/regression/cbmc-shadow-memory/static1/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdlib.h>
+
+extern int nondet_int();
+
+void main()
+{
+  __CPROVER_field_decl_global("field", (unsigned __CPROVER_bitvector[2])0);
+
+  static unsigned long int y;
+
+  assert(__CPROVER_get_field(&y, "field") == 0);
+
+  __CPROVER_set_field(&y, "field", 2u);
+  assert(__CPROVER_get_field(&y, "field") == 2u);
+}
diff --git a/regression/cbmc-shadow-memory/static1/test.desc b/regression/cbmc-shadow-memory/static1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/static1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/strdup1/main.c b/regression/cbmc-shadow-memory/strdup1/main.c
new file mode 100644
index 00000000000..b937b83bc97
--- /dev/null
+++ b/regression/cbmc-shadow-memory/strdup1/main.c
@@ -0,0 +1,33 @@
+#include <assert.h>
+#include <stdlib.h>
+#include <string.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (unsigned __CPROVER_bitvector[2])0);
+  __CPROVER_field_decl_global("field1", (unsigned __CPROVER_bitvector[2])0);
+
+  char *s = (char *)malloc(3 * sizeof(char));
+  assert(__CPROVER_get_field(&s[0], "field1") == 0);
+  assert(__CPROVER_get_field(&s[1], "field1") == 0);
+
+  __CPROVER_set_field(&s[0], "field1", 1);
+  __CPROVER_set_field(&s[1], "field1", 1);
+  assert(__CPROVER_get_field(&s[0], "field1") == 1);
+  assert(__CPROVER_get_field(&s[1], "field1") == 1);
+
+  // The shadow memories of the source and destination buffers
+  // are independent.
+  char *d = strdup(s);
+  assert(__CPROVER_get_field(&s[0], "field1") == 1);
+  assert(__CPROVER_get_field(&s[1], "field1") == 1);
+  assert(__CPROVER_get_field(&d[0], "field1") == 0);
+  assert(__CPROVER_get_field(&d[1], "field1") == 0);
+
+  __CPROVER_set_field(&d[0], "field1", 2);
+  __CPROVER_set_field(&d[1], "field1", 2);
+  assert(__CPROVER_get_field(&d[0], "field1") == 2);
+  assert(__CPROVER_get_field(&d[1], "field1") == 2);
+  assert(__CPROVER_get_field(&s[0], "field1") == 1);
+  assert(__CPROVER_get_field(&s[1], "field1") == 1);
+}
diff --git a/regression/cbmc-shadow-memory/strdup1/test.desc b/regression/cbmc-shadow-memory/strdup1/test.desc
new file mode 100644
index 00000000000..438d68ba0b0
--- /dev/null
+++ b/regression/cbmc-shadow-memory/strdup1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+--unwind 4
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/struct-get-max1/main.c b/regression/cbmc-shadow-memory/struct-get-max1/main.c
new file mode 100644
index 00000000000..659cc306f07
--- /dev/null
+++ b/regression/cbmc-shadow-memory/struct-get-max1/main.c
@@ -0,0 +1,89 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct INNERSTRUCT
+{
+  int x1;
+  int x2[2];
+};
+
+struct STRUCT
+{
+  struct INNERSTRUCT x[3];
+  int y;
+};
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (__CPROVER_bitvector[6])0);
+
+  struct STRUCT s;
+
+  __CPROVER_set_field(&(s.x[0].x1), "field1", 1);
+  assert(__CPROVER_get_field(&s, "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0]), "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0].x1), "field1") == 1);
+  // Not allowed: assert(__CPROVER_get_field(s.x[0].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[1].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[2].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.y), "field1") == 0);
+
+  __CPROVER_set_field(&(s.y), "field1", 2);
+  assert(__CPROVER_get_field(&s, "field1") == 2);
+  assert(__CPROVER_get_field(&(s.x[0]), "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0].x1), "field1") == 1);
+  // Not allowed: assert(__CPROVER_get_field(s.x[0].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[1].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[2].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.y), "field1") == 2);
+
+  __CPROVER_set_field(&(s.x[1].x2[0]), "field1", 3);
+  assert(__CPROVER_get_field(&s, "field1") == 3);
+  assert(__CPROVER_get_field(&(s.x[0]), "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0].x1), "field1") == 1);
+  // Not allowed: assert(__CPROVER_get_field(s.x[0].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[1].x2, "field1") == 3);
+  assert(__CPROVER_get_field(&(s.x[1].x2[0]), "field1") == 3);
+  assert(__CPROVER_get_field(&(s.x[1].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[2].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.y), "field1") == 2);
+
+  __CPROVER_set_field(&(s.x[2].x2[1]), "field1", 4);
+  assert(__CPROVER_get_field(&s, "field1") == 4);
+  assert(__CPROVER_get_field(&(s.x[0]), "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0].x1), "field1") == 1);
+  // Not allowed: assert(__CPROVER_get_field(s.x[0].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[1].x2, "field1") == 3);
+  assert(__CPROVER_get_field(&(s.x[1].x2[0]), "field1") == 3);
+  assert(__CPROVER_get_field(&(s.x[1].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[2].x2, "field1") == 4);
+  assert(__CPROVER_get_field(&(s.x[2].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[1]), "field1") == 4);
+  assert(__CPROVER_get_field(&(s.y), "field1") == 2);
+}
diff --git a/regression/cbmc-shadow-memory/struct-get-max1/test.desc b/regression/cbmc-shadow-memory/struct-get-max1/test.desc
new file mode 100644
index 00000000000..29c4483cdfb
--- /dev/null
+++ b/regression/cbmc-shadow-memory/struct-get-max1/test.desc
@@ -0,0 +1,9 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
diff --git a/regression/cbmc-shadow-memory/struct-get-or1/main.c b/regression/cbmc-shadow-memory/struct-get-or1/main.c
new file mode 100644
index 00000000000..0c854807fdf
--- /dev/null
+++ b/regression/cbmc-shadow-memory/struct-get-or1/main.c
@@ -0,0 +1,89 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct INNERSTRUCT
+{
+  int x1;
+  int x2[2];
+};
+
+struct STRUCT
+{
+  struct INNERSTRUCT x[3];
+  int y;
+};
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+
+  struct STRUCT s;
+
+  __CPROVER_set_field(&(s.x[0].x1), "field1", 1);
+  assert(__CPROVER_get_field(&s, "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0]), "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0].x1), "field1") == 1);
+  // Not allowed: assert(__CPROVER_get_field(s.x[0].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[1].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[2].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.y), "field1") == 0);
+
+  __CPROVER_set_field(&(s.y), "field1", 1);
+  assert(__CPROVER_get_field(&s, "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0]), "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0].x1), "field1") == 1);
+  // Not allowed: assert(__CPROVER_get_field(s.x[0].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x1), "field1") == 0);
+  // assert(__CPROVER_get_field(s.x[1].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[2].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.y), "field1") == 1);
+
+  __CPROVER_set_field(&(s.x[1].x2[0]), "field1", 1);
+  assert(__CPROVER_get_field(&s, "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0]), "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0].x1), "field1") == 1);
+  // Not allowed: assert(__CPROVER_get_field(s.x[0].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[1].x2, "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[1].x2[0]), "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[1].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[2].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.y), "field1") == 1);
+
+  __CPROVER_set_field(&(s.x[2].x2[1]), "field1", 1);
+  assert(__CPROVER_get_field(&s, "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0]), "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[0].x1), "field1") == 1);
+  // Not allowed: assert(__CPROVER_get_field(s.x[0].x2, "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[0].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[1].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[1].x2, "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[1].x2[0]), "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[1].x2[1]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x1), "field1") == 0);
+  // Not allowed: assert(__CPROVER_get_field(s.x[2].x2, "field1") == 1);
+  assert(__CPROVER_get_field(&(s.x[2].x2[0]), "field1") == 0);
+  assert(__CPROVER_get_field(&(s.x[2].x2[1]), "field1") == 1);
+  assert(__CPROVER_get_field(&(s.y), "field1") == 1);
+}
diff --git a/regression/cbmc-shadow-memory/struct-get-or1/test.desc b/regression/cbmc-shadow-memory/struct-get-or1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/struct-get-or1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/struct-set1/main.c b/regression/cbmc-shadow-memory/struct-set1/main.c
new file mode 100644
index 00000000000..91c8262e250
--- /dev/null
+++ b/regression/cbmc-shadow-memory/struct-set1/main.c
@@ -0,0 +1,74 @@
+#include <assert.h>
+
+struct INNERSTRUCT
+{
+  int x1;
+  char x2[2];
+};
+
+struct STRUCT
+{
+  struct INNERSTRUCT x[3];
+  int y;
+};
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+
+  struct STRUCT s;
+  __CPROVER_set_field(&s, "field1", (_Bool)1);
+  assert(__CPROVER_get_field(&s.x[0], "field1"));
+  assert(__CPROVER_get_field(&s.x[0].x1, "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[0].x1) + 1), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[0].x1) + 2), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[0].x1) + 3), "field1"));
+  assert(__CPROVER_get_field(&s.x[0].x2[0], "field1"));
+  assert(__CPROVER_get_field(&s.x[0].x2[1], "field1"));
+  assert(__CPROVER_get_field(&s.x[1], "field1"));
+  assert(__CPROVER_get_field(&s.x[1].x1, "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[1].x1) + 1), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[1].x1) + 2), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[1].x1) + 3), "field1"));
+  assert(__CPROVER_get_field(&s.x[1].x2[0], "field1"));
+  assert(__CPROVER_get_field(&s.x[1].x2[1], "field1"));
+  assert(__CPROVER_get_field(&s.x[2], "field1"));
+  assert(__CPROVER_get_field(&s.x[2].x1, "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[2].x1) + 1), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[2].x1) + 2), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[2].x1) + 3), "field1"));
+  assert(__CPROVER_get_field(&s.x[2].x2[0], "field1"));
+  assert(__CPROVER_get_field(&s.x[2].x2[1], "field1"));
+  assert(__CPROVER_get_field(&s.y, "field1"));
+  assert(__CPROVER_get_field((((char *)&s.y) + 1), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.y) + 2), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.y) + 3), "field1"));
+
+  __CPROVER_set_field(&s.x[1], "field1", (_Bool)0);
+  assert(__CPROVER_get_field(&s.x[0], "field1"));
+  assert(__CPROVER_get_field(&s.x[0].x1, "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[0].x1) + 1), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[0].x1) + 2), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[0].x1) + 3), "field1"));
+  assert(__CPROVER_get_field(&s.x[0].x2[0], "field1"));
+  assert(__CPROVER_get_field(&s.x[0].x2[1], "field1"));
+  assert(!__CPROVER_get_field(&s.x[1], "field1"));
+  assert(!__CPROVER_get_field(&s.x[1].x1, "field1"));
+  assert(!__CPROVER_get_field((((char *)&s.x[1].x1) + 1), "field1"));
+  assert(!__CPROVER_get_field((((char *)&s.x[1].x1) + 2), "field1"));
+  assert(!__CPROVER_get_field((((char *)&s.x[1].x1) + 3), "field1"));
+  assert(!__CPROVER_get_field(&s.x[1].x2[0], "field1"));
+  assert(!__CPROVER_get_field(&s.x[1].x2[1], "field1"));
+  assert(__CPROVER_get_field(&s.x[2], "field1"));
+  assert(__CPROVER_get_field(&s.x[2].x1, "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[2].x1) + 1), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[2].x1) + 2), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.x[2].x1) + 3), "field1"));
+  assert(__CPROVER_get_field(&s.x[2].x2[0], "field1"));
+  assert(__CPROVER_get_field(&s.x[2].x2[1], "field1"));
+  assert(__CPROVER_get_field(&s.y, "field1"));
+  assert(__CPROVER_get_field((((char *)&s.y) + 1), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.y) + 2), "field1"));
+  assert(__CPROVER_get_field((((char *)&s.y) + 3), "field1"));
+  return 0;
+}
diff --git a/regression/cbmc-shadow-memory/struct-set1/test.desc b/regression/cbmc-shadow-memory/struct-set1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/struct-set1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/taint-example1/main.c b/regression/cbmc-shadow-memory/taint-example1/main.c
new file mode 100644
index 00000000000..d17af08b3d1
--- /dev/null
+++ b/regression/cbmc-shadow-memory/taint-example1/main.c
@@ -0,0 +1,75 @@
+#include <assert.h>
+#include <string.h>
+
+extern int nondet_int();
+
+int append(char *buf, int pos, char *src)
+{
+  int len = strlen(src);
+  for(int i = 0; i < len; ++i)
+  {
+    buf[pos + i] = src[i];
+    // propagate taint
+    __CPROVER_set_field(
+      &buf[pos + i], "tainted", __CPROVER_get_field(&src[i], "tainted"));
+  }
+  return pos + len;
+}
+
+void encode(char *buf, char *uname, char *passwd)
+{
+  int pos = append(buf, 0, "{\"username\":\"");
+  pos = append(buf, pos, uname);
+  pos = append(buf, pos, "\",\"password\":\"");
+  pos = append(buf, pos, passwd);
+  pos = append(buf, pos, "\"}");
+  buf[pos] = '\0';
+}
+
+void make_nondet_len_string(char *buf, _Bool taint)
+{
+  int len = nondet_int();
+  __CPROVER_assume(0 <= len && len < 8);
+  buf[len] = '\0';
+  // taint the input data
+  for(int i = 0; i < len; ++i)
+    __CPROVER_set_field(&buf[i], "tainted", taint);
+}
+
+int check_part(char *buf, int pos, char *src, _Bool expected)
+{
+  int len = strlen(src);
+  for(int i = 0; i < len; ++i)
+  {
+    _Bool actual = __CPROVER_get_field(&buf[pos + i], "tainted");
+    assert(actual == expected);
+  }
+  return pos + len;
+}
+
+void check(char *buf, char *uname, char *passwd)
+{
+  int pos = check_part(buf, 0, "{\"username\":\"", 0);
+  pos = check_part(buf, pos, uname, 0);
+  pos = check_part(buf, pos, "\",\"password\":\"", 0);
+  pos = check_part(buf, pos, passwd, 1);
+  pos = check_part(buf, pos, "\"}", 0);
+  check_part(buf, pos, "\0", 0);
+}
+
+void main()
+{
+  // declare shadow fields
+  __CPROVER_field_decl_local("tainted", (_Bool)0);
+  __CPROVER_field_decl_global("tainted", (_Bool)0);
+  // create harness for SUT
+  char uname[8];
+  char passwd[8];
+  make_nondet_len_string(uname, 0);  // untainted
+  make_nondet_len_string(passwd, 1); // tainted
+  // call SUT
+  char json[46];
+  encode(json, uname, passwd);
+  // check properties
+  check(json, uname, passwd);
+}
diff --git a/regression/cbmc-shadow-memory/taint-example1/test.desc b/regression/cbmc-shadow-memory/taint-example1/test.desc
new file mode 100644
index 00000000000..cb611a28bb6
--- /dev/null
+++ b/regression/cbmc-shadow-memory/taint-example1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+--unwind 15
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/trace1/main.c b/regression/cbmc-shadow-memory/trace1/main.c
new file mode 100644
index 00000000000..084555b696a
--- /dev/null
+++ b/regression/cbmc-shadow-memory/trace1/main.c
@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+
+  int x;
+
+  // create a non-trivial counterexample trace
+  for(int i = 0; i < 4; ++i)
+  {
+    if(i == 2)
+    {
+      __CPROVER_set_field(&x, "field1", 1);
+    }
+  }
+
+  assert(__CPROVER_get_field(&x, "field1") == 0);
+}
diff --git a/regression/cbmc-shadow-memory/trace1/test.desc b/regression/cbmc-shadow-memory/trace1/test.desc
new file mode 100644
index 00000000000..d717cd26938
--- /dev/null
+++ b/regression/cbmc-shadow-memory/trace1/test.desc
@@ -0,0 +1,9 @@
+FUTURE
+main.c
+--stop-on-fail --unwind 5
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED
+SM__&x!0@1__field1=
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/union-get-max1/main.c b/regression/cbmc-shadow-memory/union-get-max1/main.c
new file mode 100644
index 00000000000..90ac1b5a70a
--- /dev/null
+++ b/regression/cbmc-shadow-memory/union-get-max1/main.c
@@ -0,0 +1,81 @@
+#include <assert.h>
+#include <stdlib.h>
+
+union UNIONNAME
+{
+  int x1;
+  struct
+  {
+    char y1;
+    // char padding;
+    short y2;
+    short y3;
+  } x2;
+  char x3[3];
+};
+
+int main()
+{
+  __CPROVER_field_decl_local("field2", (__CPROVER_bitvector[6])0);
+
+  union UNIONNAME u;
+
+  assert(__CPROVER_get_field(&u, "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x1), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y3), "field2") == 0);
+  // Not allowed: assert(__CPROVER_get_field(u.x3, "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 0);
+
+  __CPROVER_set_field(&(u.x1), "field2", 1);
+  assert(__CPROVER_get_field(&u, "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x1), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2.y3), "field2") == 0);
+  // Not allowed: assert(__CPROVER_get_field(u.x3, "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 1);
+
+  __CPROVER_set_field(&(u.x2.y1), "field2", 2);
+  assert(__CPROVER_get_field(&u, "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x1), "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x2), "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2.y3), "field2") == 0);
+  // Not allowed: assert(__CPROVER_get_field(u.x3, "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 1);
+
+  __CPROVER_set_field(&(u.x2.y2), "field2", 3);
+  assert(__CPROVER_get_field(&u, "field2") == 3);
+  assert(__CPROVER_get_field(&(u.x1), "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x2), "field2") == 3);
+  assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 3);
+  assert(__CPROVER_get_field(&(u.x2.y3), "field2") == 0);
+  // Not allowed: assert(__CPROVER_get_field(u.x3, "field2") == 3);
+  assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 3);
+
+  __CPROVER_set_field(&(u.x2.y3), "field2", 4);
+  assert(__CPROVER_get_field(&u, "field2") == 4);
+  assert(__CPROVER_get_field(&(u.x1), "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x2), "field2") == 4);
+  assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 3);
+  assert(__CPROVER_get_field(&(u.x2.y3), "field2") == 4);
+  // Not allowed: assert(__CPROVER_get_field(u.x3, "field2") == 3);
+  assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 2);
+  assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 3);
+}
diff --git a/regression/cbmc-shadow-memory/union-get-max1/test.desc b/regression/cbmc-shadow-memory/union-get-max1/test.desc
new file mode 100644
index 00000000000..a7f9f044e8e
--- /dev/null
+++ b/regression/cbmc-shadow-memory/union-get-max1/test.desc
@@ -0,0 +1,10 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Not implemented yet.
diff --git a/regression/cbmc-shadow-memory/union-get-or1/main.c b/regression/cbmc-shadow-memory/union-get-or1/main.c
new file mode 100644
index 00000000000..922ae4f0b98
--- /dev/null
+++ b/regression/cbmc-shadow-memory/union-get-or1/main.c
@@ -0,0 +1,80 @@
+#include <assert.h>
+#include <stdlib.h>
+
+union UNIONNAME
+{
+  int x1;
+  struct
+  {
+    char y1;
+    // char padding;
+    short y2;
+    short y3;
+  } x2;
+  char x3[3];
+};
+
+int main()
+{
+  __CPROVER_field_decl_local("field2", (_Bool)0);
+
+  union UNIONNAME u;
+  assert(__CPROVER_get_field(&u, "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x1), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y3), "field2") == 0);
+  // Not allowed: assert(__CPROVER_get_field(u.x3, "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 0);
+
+  __CPROVER_set_field(&(u.x1), "field2", 1);
+  assert(__CPROVER_get_field(&u, "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x1), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2.y3), "field2") == 0);
+  // Not allowed: assert(__CPROVER_get_field(u.x3, "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 1);
+
+  __CPROVER_set_field(&(u.x2.y1), "field2", 0);
+  assert(__CPROVER_get_field(&u, "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x1), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2.y3), "field2") == 0);
+  // Not allowed: assert(__CPROVER_get_field(u.x3, "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 1);
+
+  __CPROVER_set_field(&(u.x2.y2), "field2", 0);
+  assert(__CPROVER_get_field(&u, "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x1), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y3), "field2") == 0);
+  // Not allowed: assert(__CPROVER_get_field(u.x3, "field2") == 7);
+  assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 0);
+
+  __CPROVER_set_field(&(u.x2.y3), "field2", 1);
+  assert(__CPROVER_get_field(&u, "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x1), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x2.y1), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y2), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x2.y3), "field2") == 1);
+  // Not allowed: assert(__CPROVER_get_field(u.x3, "field2") == 7);
+  assert(__CPROVER_get_field(&(u.x3[0]), "field2") == 0);
+  assert(__CPROVER_get_field(&(u.x3[1]), "field2") == 1);
+  assert(__CPROVER_get_field(&(u.x3[2]), "field2") == 0);
+}
diff --git a/regression/cbmc-shadow-memory/union-get-or1/test.desc b/regression/cbmc-shadow-memory/union-get-or1/test.desc
new file mode 100644
index 00000000000..20cb1b9a001
--- /dev/null
+++ b/regression/cbmc-shadow-memory/union-get-or1/test.desc
@@ -0,0 +1,10 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+
diff --git a/regression/cbmc-shadow-memory/union-set1/main.c b/regression/cbmc-shadow-memory/union-set1/main.c
new file mode 100644
index 00000000000..1f2897663fb
--- /dev/null
+++ b/regression/cbmc-shadow-memory/union-set1/main.c
@@ -0,0 +1,52 @@
+#include <assert.h>
+
+union UNIONNAME
+{
+  int x1;
+  struct
+  {
+    char y1;
+    // char padding;
+    short y2;
+    short y3;
+  } x2;
+  char x3[3];
+};
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+
+  union UNIONNAME u;
+
+  __CPROVER_set_field(&u, "field1", (_Bool)1);
+  assert(__CPROVER_get_field(&u.x1, "field1"));
+  assert(__CPROVER_get_field((((char *)&u.x1) + 1), "field1"));
+  assert(__CPROVER_get_field((((char *)&u.x1) + 2), "field1"));
+  assert(__CPROVER_get_field((((char *)&u.x1) + 3), "field1"));
+  assert(__CPROVER_get_field(&u.x2, "field1"));
+  assert(__CPROVER_get_field(&u.x2.y1, "field1"));
+  assert(__CPROVER_get_field(&u.x2.y2, "field1"));
+  assert(__CPROVER_get_field((((char *)&u.x2.y2) + 1), "field1"));
+  assert(__CPROVER_get_field(&u.x2.y3, "field1"));
+  assert(__CPROVER_get_field((((char *)&u.x2.y3) + 1), "field1"));
+  assert(__CPROVER_get_field(&u.x3[0], "field1"));
+  assert(__CPROVER_get_field(&u.x3[1], "field1"));
+  assert(__CPROVER_get_field(&u.x3[2], "field1"));
+
+  __CPROVER_set_field(&u.x2, "field1", (_Bool)0);
+  assert(!__CPROVER_get_field(&u.x1, "field1"));
+  assert(!__CPROVER_get_field((((char *)&u.x1) + 1), "field1"));
+  assert(!__CPROVER_get_field((((char *)&u.x1) + 2), "field1"));
+  assert(!__CPROVER_get_field((((char *)&u.x1) + 3), "field1"));
+  assert(!__CPROVER_get_field(&u.x2, "field1"));
+  assert(!__CPROVER_get_field(&u.x2.y1, "field1"));
+  assert(!__CPROVER_get_field(&u.x2.y2, "field1"));
+  assert(!__CPROVER_get_field((((char *)&u.x2.y2) + 1), "field1"));
+  assert(!__CPROVER_get_field(&u.x2.y3, "field1"));
+  assert(!__CPROVER_get_field((((char *)&u.x2.y3) + 1), "field1"));
+  assert(!__CPROVER_get_field(&u.x3[0], "field1"));
+  assert(!__CPROVER_get_field(&u.x3[1], "field1"));
+  assert(!__CPROVER_get_field(&u.x3[2], "field1"));
+  return 0;
+}
diff --git a/regression/cbmc-shadow-memory/union-set1/test.desc b/regression/cbmc-shadow-memory/union-set1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/union-set1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/var-assign1/main.c b/regression/cbmc-shadow-memory/var-assign1/main.c
new file mode 100644
index 00000000000..e80db064443
--- /dev/null
+++ b/regression/cbmc-shadow-memory/var-assign1/main.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("field", (_Bool)0);
+
+  _Bool z;
+  int x;
+  __CPROVER_set_field(&x, "field", z);
+  assert(__CPROVER_get_field(&x, "field") == z);
+}
diff --git a/regression/cbmc-shadow-memory/var-assign1/test.desc b/regression/cbmc-shadow-memory/var-assign1/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/var-assign1/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-shadow-memory/void-ptr-param-get1/main.c b/regression/cbmc-shadow-memory/void-ptr-param-get1/main.c
new file mode 100644
index 00000000000..b553f5eef3d
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc-shadow-memory/void-ptr-param-get1/test.desc b/regression/cbmc-shadow-memory/void-ptr-param-get1/test.desc
new file mode 100644
index 00000000000..638e2204b4b
--- /dev/null
+++ b/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
diff --git a/regression/cbmc-shadow-memory/void-ptr-param-set1/main.c b/regression/cbmc-shadow-memory/void-ptr-param-set1/main.c
new file mode 100644
index 00000000000..c20d137a476
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc b/regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc
new file mode 100644
index 00000000000..bde0b0f48e5
--- /dev/null
+++ b/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
diff --git a/regression/cbmc-shadow-memory/void-ptr-param2/main.c b/regression/cbmc-shadow-memory/void-ptr-param2/main.c
new file mode 100644
index 00000000000..36c3cf3fc9a
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc-shadow-memory/void-ptr-param2/test.desc b/regression/cbmc-shadow-memory/void-ptr-param2/test.desc
new file mode 100644
index 00000000000..aea17ee4da8
--- /dev/null
+++ b/regression/cbmc-shadow-memory/void-ptr-param2/test.desc
@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring