Add regressions for shadow memory BV aggregation

Author: Enrico Steffinlongo

regression/cbmc-shadow-memory/bv-get-max/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("uninitialized", (char)0);
+  __CPROVER_field_decl_global("uninitialized", (char)0);
+
+  int i;
+  char *a = &i;
+
+  __CPROVER_set_field(a + 1, "uninitialized", 1);
+
+  assert(__CPROVER_get_field(a, "uninitialized") == 0);
+  assert(__CPROVER_get_field(&i, "uninitialized") == 1);
+  assert(__CPROVER_get_field(a + 1, "uninitialized") == 1);
+  // Expecting the remaining bytes to be untouched by the setting of the field.
+  assert(__CPROVER_get_field(a + 2, "uninitialized") == 0);
+  assert(__CPROVER_get_field(a + 3, "uninitialized") == 0);
+}

regression/cbmc-shadow-memory/bv-get-max/test.desc

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

regression/cbmc-shadow-memory/bv-get-or/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("uninitialized", (_Bool)0);
+  __CPROVER_field_decl_global("uninitialized", (_Bool)0);
+
+  int i;
+  char *a = &i;
+
+  __CPROVER_set_field(a + 1, "uninitialized", 1);
+
+  assert(__CPROVER_get_field(a, "uninitialized") == 0);
+  assert(__CPROVER_get_field(a + 1, "uninitialized") == 1);
+  assert(__CPROVER_get_field(&i, "uninitialized") == 1);
+  // Expecting the remaining bytes to be untouched by the setting of the field.
+  assert(__CPROVER_get_field(a + 2, "uninitialized") == 0);
+  assert(__CPROVER_get_field(a + 3, "uninitialized") == 0);
+}

regression/cbmc-shadow-memory/bv-get-or/test.desc

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