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

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

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 21.*SUCCESS$
+^\[main.assertion\.2\] line 24.*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-sensitivity2/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-sensitivity3/test.c

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

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

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 9.*SUCCESS$
+^\[main.assertion\.2\] line 10.*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-sensitivity4/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-sensitivity5/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-sensitivity6/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-sensitivity7/test.c

@@ -7,5 +7,6 @@ int main(int argc, char **argv)
   char *ptr = argc % 2 ? (char *)&array[0] : (char *)&argc;
   ptr[argc] = 'a';
   ptr[1] = (char)argc;
-  assert(array[1] == argc);
+  assert(ptr[1] == (char)argc);
+  assert(array[1] == (char)argc);
 }

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

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 10.*SUCCESS$
+^\[main.assertion\.2\] line 11.*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-sensitivity8/test.c

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

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

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 11.*SUCCESS$
+^\[main.assertion\.2\] line 12.*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-sensitivity9/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.