Add tests for filtering shadow memory

The --no-shadow-memory-matching option will allow
to avoid the allocation of shadow memory for matching
variables.

Author: peterschrammel

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

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