Adding regression tests for large step encoding of CHCs

Author: Yakir Vizel

regression/cprover/large_step/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cprover>"
+)

regression/cprover/large_step/Makefile

@@ -0,0 +1,14 @@
+default: test-no-p
+
+include ../../../src/config.inc
+include ../../../src/common
+
+test:
+	@../../test.pl -e -p -c '../../../../src/cprover/cprover --large-step'
+
+test-no-p:
+	@../../test.pl -e -c '../../../../src/cprover/cprover --large-step'
+
+clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/cprover/large_step/arrays/array1.c

@@ -0,0 +1,10 @@
+int array[10];
+
+int main()
+{
+  array[1l] = 10;
+  array[2l] = 20;
+  __CPROVER_assert(array[1l] == 10, "property 1"); // passes
+  __CPROVER_assert(array[2l] == 20, "property 2"); // passes
+  __CPROVER_assert(array[2l] == 30, "property 3"); // fails
+}

regression/cprover/large_step/arrays/array1.desc

@@ -0,0 +1,14 @@
+CORE
+array1.c
+--text --solve --inline --no-safety
+^EXIT=10$
+^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
+^\[main\.assertion\.3\] line \d+ property 3: REFUTED$
+--

regression/cprover/large_step/arrays/array2.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int array[10];
+  int i, j, k;
+  __CPROVER_assume(i == j);
+  __CPROVER_assert(array[i] == array[j], "property 1"); // passes
+  __CPROVER_assert(array[i] == array[k], "property 2"); // fails
+}

regression/cprover/large_step/arrays/array2.desc

@@ -0,0 +1,11 @@
+CORE
+array2.c
+--text --solve --inline --no-safety
+^EXIT=10$
+^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. \(S13\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S14\(ς\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::i❞\)|cast\(ς\(❝main::1::i❞\), signedbv\[64\]\))\)\) = ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::j❞\)|cast\(ς\(❝main::1::j❞\), signedbv\[64\]\))\)\)\)$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::i❞\)|cast\(ς\(❝main::1::i❞\), signedbv\[64\]\))\)\) = ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::k❞\)|cast\(ς\(❝main::1::k❞\), signedbv\[64\]\))\)\)\)$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
+--

regression/cprover/large_step/arrays/array4.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int a[100];
+  int *p = a;
+  __CPROVER_assert(p[23] == a[23], "property 1"); // should pass
+  return 0;
+}

regression/cprover/large_step/arrays/array4.desc

@@ -0,0 +1,7 @@
+CORE
+array4.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+--

regression/cprover/large_step/arrays/array_literal1.c

@@ -0,0 +1,8 @@
+int array[10] = {0, 1, 2, 3, 4};
+
+int main()
+{
+  __CPROVER_assert(array[0l] == 0, "property 1"); // passes
+  __CPROVER_assert(array[1l] == 1, "property 2"); // passes
+  return 0;
+}

regression/cprover/large_step/arrays/array_literal1.desc

@@ -0,0 +1,8 @@
+CORE
+array_literal1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
+--