Merge pull request #6717 from diffblue/set_encoding

CHC encoder

Author: kroening

.clang-format-ignore

@@ -1,3 +1,4 @@
 jbmc/src/miniz/miniz.cpp
+src/cprover/wcwidth.c
 src/nonstd/optional.hpp
 unit/catch/catch.hpp

CMakeLists.txt

@@ -150,6 +150,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
               "$<TARGET_FILE:unit>"
               "$<TARGET_FILE:goto-harness>"
               "$<TARGET_FILE:cbmc>"
+              "$<TARGET_FILE:cprover>"
               "$<TARGET_FILE:crangler>"
               "$<TARGET_FILE:driver>"
               "$<TARGET_FILE:goto-analyzer>"
@@ -214,6 +215,8 @@ cprover_default_properties(
     cbmc
     cbmc-lib
     cpp
+    cprover
+    cprover-lib
     crangler
     crangler-lib
     driver

regression/cbmc/pointer-predicates/in_range1.c

@@ -0,0 +1,13 @@
+int x;
+
+int main()
+{
+  __CPROVER_assert(__CPROVER_pointer_in_range(&x, &x, &x), "property 1");
+  __CPROVER_assert(__CPROVER_pointer_in_range(&x, &x, &x + 1), "property 2");
+  __CPROVER_assert(
+    __CPROVER_pointer_in_range(&x, &x + 1, &x + 1), "property 3");
+  __CPROVER_assert(!__CPROVER_pointer_in_range(&x, &x + 1, &x), "property 4");
+  __CPROVER_assert(!__CPROVER_pointer_in_range(0, &x, &x), "property 5");
+  __CPROVER_assert(!__CPROVER_pointer_in_range(&x, 0, &x), "property 6");
+  __CPROVER_assert(!__CPROVER_pointer_in_range(&x, &x, 0), "property 7");
+}

regression/cbmc/pointer-predicates/in_range1.desc

@@ -0,0 +1,8 @@
+CORE
+in_range1.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/cprover/Makefile

@@ -0,0 +1,13 @@
+default: test-no-p
+
+include ../../src/config.inc
+include ../../src/common
+
+test:
+	@../test.pl -e -p -c '../../../src/cprover/cprover'
+
+test-no-p:
+	@../test.pl -e -c '../../../src/cprover/cprover'
+
+clean:
+	$(RM) tests.log

regression/cprover/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/arrays/array1.desc

@@ -0,0 +1,14 @@
+CORE
+array1.c
+--text --solve --inline --no-safety
+^EXIT=10$
+^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, 1\):=10\]\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[element_address\(❝array❞, 2\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, 1\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, 2\)\) = 20\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(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/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/arrays/array2.desc

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

regression/cprover/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;
+}