Merge pull request #5951 from tautschnig/incremental-future-tests

Add cbmc --incremental regression tests as FUTURE

Author: tautschnig

regression/CMakeLists.txt

@@ -32,6 +32,9 @@ add_subdirectory(cpp)
 add_subdirectory(cbmc-concurrency)
 add_subdirectory(cbmc-cover)
 add_subdirectory(cbmc-incr-oneloop)
+add_subdirectory(cbmc-incr)
+add_subdirectory(cbmc-with-incr)
+add_subdirectory(array-refinement-with-incr)
 add_subdirectory(goto-instrument-typedef)
 add_subdirectory(smt2_solver)
 add_subdirectory(smt2_strings)

regression/Makefile

@@ -10,6 +10,9 @@ DIRS = cbmc \
        cbmc-concurrency \
        cbmc-cover \
        cbmc-incr-oneloop \
+       cbmc-incr \
+       cbmc-with-incr \
+       array-refinement-with-incr \
        goto-instrument-typedef \
        smt2_solver \
        smt2_strings \

regression/array-refinement-with-incr/Array_UF1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 11
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF10/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 1
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF11/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 1
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF12/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 2
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF13/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 1
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF14/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 6
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF15/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 11
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF16/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 2
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF17/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 9
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF18/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 11
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF19/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 3
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 5
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF20/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 12
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF3/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 3 --no-unwinding-assertions
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF4/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 2
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF5/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 2
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF6/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 3
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF7/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 3
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF8/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 6
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF9/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 21
 ^EXIT=10$

regression/array-refinement-with-incr/CMakeLists.txt

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

regression/cbmc-incr/Ackermann02_false1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --error-label ERROR --unwind-max 6
 ^EXIT=10$

regression/cbmc-incr/MultCommutative_true1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --error-label ERROR --unwind-max 6 --no-unwinding-assertions
 ^EXIT=0$

regression/cbmc-incr/alarm1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --unwind-max 25 --no-unwinding-assertions
 ^EXIT=0$

regression/cbmc-incr/alarm2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --unwind-min 5 --unwind-max 10 --no-unwinding-assertions
 ^EXIT=10$

regression/cbmc-incr/alarm3/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=10$

regression/cbmc-incr/arrays2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --unwind-max 5  --no-unwinding-assertions --arrays-uf-always
 ^EXIT=10$

regression/cbmc-incr/arrays3/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions
 ^EXIT=0$

regression/cbmc-incr/arrays4/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions
 ^EXIT=0$

regression/cbmc-incr/arrays5/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --unwind-max 5 --no-unwinding-assertions --arrays-uf-always
 ^EXIT=0$

regression/cbmc-incr/assertion-after-loop1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --unwind-max 10
 ^EXIT=10$

regression/cbmc-incr/assertion-after-loop2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions --unwind-max 10
 ^EXIT=0$

regression/cbmc-incr/cruise1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --unwind-max 10 --no-unwinding-assertions
 ^EXIT=0$

regression/cbmc-incr/cruise2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=10$

regression/cbmc-incr/email_spec27_product31_false1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --error-label ERROR --unwind-max 3
 ^EXIT=10$

regression/cbmc-incr/induction1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --stop-when-unsat --no-unwinding-assertions
 ^EXIT=0$

regression/cbmc-incr/magic1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --magic-numbers
 ^EXIT=0$

regression/cbmc-incr/minmaxunwind1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions --unwind-min 4 --unwind-max 6
 ^EXIT=10$

regression/cbmc-incr/minmaxunwind2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions --unwind-min 5 --unwind-max 5
 ^EXIT=10$

regression/cbmc-incr/minmaxunwind3/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions --unwind-min 2 --unwind-max 4
 ^EXIT=0$

regression/cbmc-incr/minmaxunwind4/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions --unwind-min 6 --unwind-max 8
 ^EXIT=10$

regression/cbmc-incr/minmaxunwind5/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions --unwind-min 4
 ^EXIT=10$

regression/cbmc-incr/moreasserts1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=10$

regression/cbmc-incr/moreloops1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=10$

regression/cbmc-incr/nestedloop1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=10$

regression/cbmc-incr/no-unwinding-assertion1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions --unwind-max 10
 ^EXIT=0$

regression/cbmc-incr/recursion1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=0$

regression/cbmc-incr/recursion2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=0$

regression/cbmc-incr/simpleloop1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=10$

regression/cbmc-incr/simpleloop2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --unwind-max 6 --no-unwinding-assertions
 ^EXIT=10$

regression/cbmc-incr/simpleloop3/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/cbmc-incr/simpleloopmax1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions --unwind-max 10
 ^EXIT=10$

regression/cbmc-incr/simpleloopmax2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --no-unwinding-assertions --unwind-max 10
 ^EXIT=0$

regression/cbmc-incr/simplifier1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --unwind-max 5 --no-unwinding-assertions
 ^EXIT=0$

regression/cbmc-incr/simplifier2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --unwind-max 3 --no-unwinding-assertions
 ^EXIT=0$

regression/cbmc-incr/simplifier3/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --unwind-max 5 --no-unwinding-assertions
 ^EXIT=0$

regression/cbmc-incr/sum_array_true1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --error-label ERROR --unwind-max 6 --no-unwinding-assertions
 ^EXIT=0$

regression/cbmc-incr/unwind-not-forever1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=10$

regression/cbmc-incr/unwind-not-forever2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=0$

regression/cbmc-incr/unwinding-assertion1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --unwind-max 10
 ^EXIT=10$

regression/cbmc-incr/verisec_OpenSER__cases1_stripFullBoth_arr_false1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --error-label ERROR --unwind-max 6
 ^EXIT=10$

regression/cbmc-with-incr/ASHR1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=0$

regression/cbmc-with-incr/Address_of1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 
 ^EXIT=0$