Merge pull request #7180 from diffblue/cprover-regression

enable cprover regression tests

Author: tautschnig

regression/CMakeLists.txt

@@ -26,6 +26,7 @@ endmacro(add_test_pl_tests)
 add_subdirectory(cbmc)
 add_subdirectory(cbmc-library)
 add_subdirectory(goto-analyzer)
+add_subdirectory(cprover)
 add_subdirectory(ansi-c)
 add_subdirectory(goto-instrument)
 add_subdirectory(cpp)

regression/Makefile

@@ -3,6 +3,7 @@
 # listed with decreasing runtimes (i.e. longest running at the top)
 DIRS = cbmc \
        cbmc-library \
+       cprover \
        crangler \
        goto-analyzer \
        ansi-c \

regression/cprover/CMakeLists.txt

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

regression/cprover/arrays/array1.desc

@@ -3,11 +3,11 @@ 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\)$
+^\(\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/function_pointers/malloc_wrapper.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 malloc_wrapper.c
 
 ^EXIT=0$

regression/cprover/safety/dynamic_object1.c

@@ -1,6 +1,6 @@
 int main()
 {
-  void *p, *q;
+  char *p, *q;
   // functional consistency of dynamic_object
   __CPROVER_assume(p == q);
 

regression/cprover/safety/live_object1.c

@@ -1,6 +1,6 @@
 int main()
 {
-  void *p, *q;
+  char *p, *q;
   // functional consistency of live_object
   __CPROVER_assume(__CPROVER_LIVE_OBJECT(p));
   __CPROVER_assume(p == q);

regression/cprover/safety/object_size1.c

@@ -1,6 +1,6 @@
 int main()
 {
-  void *p, *q;
+  char *p, *q;
   // functional consistency of object_size
   __CPROVER_assume(p == q);