Add tests for shadow memory output in trace

Shadow memory assignments appear in trace.

Author: peterschrammel

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);
+}

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