Merge pull request #7002 from esteffin/esteffin/non-smt2-standard-array-support

Regression tests for non-SMT2.6-standard array support

Author: Enrico Steffinlongo

regression/cbmc-incr-smt2/arrays/bool_array_write.c

@@ -0,0 +1,9 @@
+int main()
+{
+  __CPROVER_bool bool_array[100];
+  unsigned int index;
+  __CPROVER_assume(index < 10000);
+  bool_array[index] = 1;
+  __CPROVER_assert(bool_array[index], "Array condition");
+  __CPROVER_assert(!bool_array[index], "Array condition");
+}

regression/cbmc-incr-smt2/arrays/bool_array_write.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+bool_array_write.c
+
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line \d+ Array condition: SUCCESS
+\[main\.assertion\.2\] line \d+ Array condition: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of updating the value at an index of a __CPROVER_bool (boolean) array.

regression/cbmc-incr-smt2/arrays/multi_dimension_array_write.c

@@ -0,0 +1,11 @@
+int main()
+{
+  int example_array[10000][2000];
+  unsigned int index_i;
+  unsigned int index_j;
+  __CPROVER_assume(index_i < 10000);
+  __CPROVER_assume(index_j < 2000);
+  example_array[index_i][index_j] = 42;
+  __CPROVER_assert(example_array[index_i][index_j] == 42, "Array condition");
+  __CPROVER_assert(example_array[index_i][index_j] != 42, "Array condition");
+}

regression/cbmc-incr-smt2/arrays/multi_dimension_array_write.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+multi_dimension_array_write.c
+
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line \d+ Array condition: SUCCESS
+\[main\.assertion\.2\] line \d+ Array condition: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of updating the value at an index of a __CPROVER_bool (boolean) array.