Add tests for shadow memory for string constants

Const char * parameters and
pointers into string constants.

Author: peterschrammel

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

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

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

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