Add tests for gathering shadow memory declarations

Check that right/wrong shadow memory declarations
are accepted/rejected.

Author: peterschrammel

regression/cbmc-shadow-memory/declarations1/bad1.c

@@ -0,0 +1,4 @@
+void bad_declaration1()
+{
+  __CPROVER_field_decl_local("field1", (int)0);
+}

regression/cbmc-shadow-memory/declarations1/bad2.c

@@ -0,0 +1,8 @@
+void bad_declaration2()
+{
+  struct STRUCT
+  {
+    char x;
+  } s;
+  __CPROVER_field_decl_global("field2", s);
+}

regression/cbmc-shadow-memory/declarations1/good.c

@@ -0,0 +1,5 @@
+void good_declarations()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+  __CPROVER_field_decl_global("field2", (unsigned __CPROVER_bitvector[6])0);
+}

regression/cbmc-shadow-memory/declarations1/test_bad1.desc

@@ -0,0 +1,9 @@
+CORE
+bad1.c
+--function bad_declaration1 --verbosity 10
+^EXIT=6$
+^SIGNAL=0$
+^A shadow memory field must not be larger than 8 bits.
+--
+--
+Test that a shadow memory declaration of a too large type is rejected.

regression/cbmc-shadow-memory/declarations1/test_bad2.desc

@@ -0,0 +1,9 @@
+CORE
+bad2.c
+--function bad_declaration2 --verbosity 10
+^EXIT=6$
+^SIGNAL=0$
+^A shadow memory field must be of a bitvector type.
+--
+--
+Test that a shadow memory declaration of a non-bitvector type is rejected.

regression/cbmc-shadow-memory/declarations1/test_good.desc

@@ -0,0 +1,12 @@
+CORE
+good.c
+--function good_declarations --verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^Shadow memory: declare local field field1 of type c_bool\[8\]
+^Shadow memory: declare global field field2 of type unsignedbv\[6\]
+--
+^A shadow memory field must
+--
+Test that shadow memory declarations are correctly gathered.