Add execution tests for array-cell-sensitivity

These are companions to the existing tests that check the show-vcc output, and serve to check
that the formulas generated appear to behave properly.

Author: smowton

regression/cbmc/array-cell-sensitivity1/test_execution.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.

regression/cbmc/array-cell-sensitivity10/test.c

@@ -9,8 +9,10 @@ struct A
 int main(int argc, char **argv)
 {
   struct A array[10];
-  struct A *ptr = argc % 2 ? (struct A *)&argc : &array[0];
+  struct A other[2];
+  struct A *ptr = argc % 2 ? &other : &array[0];
   ptr[argc].x = 1;
   ptr[1].x = argc;
+  assert(ptr[1].x == argc);
   assert(array[1].x == argc);
 }

regression/cbmc/array-cell-sensitivity10/test_execution.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 16.*SUCCESS$
+^\[main.assertion\.2\] line 17.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.

regression/cbmc/array-cell-sensitivity11/test.c

@@ -11,5 +11,6 @@ int main(int argc, char **argv)
   struct A array[10];
   int *ptr = argc % 2 ? &argc : &array[0].y;
   *ptr = argc;
+  assert(*ptr == argc);
   assert(array[1].y == argc);
 }

regression/cbmc/array-cell-sensitivity11/test_execution.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 14.*SUCCESS$
+^\[main.assertion\.2\] line 15.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.

regression/cbmc/array-cell-sensitivity12/test.c

@@ -11,5 +11,6 @@ int main(int argc, char **argv)
   struct A array[10];
   int *ptr = argc % 2 ? &array[0].x : &array[0].y;
   *ptr = argc;
+  assert(*ptr == argc);
   assert(array[0].y == argc);
 }

regression/cbmc/array-cell-sensitivity12/test_execution.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 14.*SUCCESS$
+^\[main.assertion\.2\] line 15.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.

regression/cbmc/array-cell-sensitivity13/test.c

@@ -17,5 +17,6 @@ int main(int argc, char **argv)
   node2.children[0] = argc % 11 ? &node1 : &node2;
   node2.children[1] = argc % 13 ? &node1 : &node2;
   root.children[0]->children[1]->children[1]->children[0]->data = 1;
+  assert(root.children[0]->children[1]->children[1]->children[0]->data == 1);
   assert(node1.data == argc);
 }

regression/cbmc/array-cell-sensitivity13/test_execution.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 20.*SUCCESS$
+^\[main.assertion\.2\] line 21.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.

regression/cbmc/array-cell-sensitivity14/test.c

@@ -18,5 +18,8 @@ int main(int argc, char **argv)
   node2.children[1] = argc % 13 ? &node1 : &node2;
   int idx1 = 0, idx2 = 1, idx3 = 1, idx4 = 0;
   root.children[idx1]->children[idx2]->children[idx3]->children[idx4]->data = 1;
+  assert(
+    root.children[idx1]->children[idx2]->children[idx3]->children[idx4]->data ==
+    1);
   assert(node1.data == argc);
 }