Merge pull request #5217 from xbauch/incremental-one-loop-rebase

Incremental unwinding of one specified loop

Author: petr-bauch

regression/CMakeLists.txt

@@ -3,7 +3,7 @@ set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
 macro(add_test_pl_profile name cmdline flag profile)
     add_test(
         NAME "${name}-${profile}"
-        COMMAND ${test_pl_path} -e -p -c ${cmdline} ${flag} ${ARGN}
+        COMMAND ${test_pl_path} -e -p -c "${cmdline}" ${flag} ${ARGN}
         WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
     )
     set_tests_properties("${name}-${profile}" PROPERTIES
@@ -31,6 +31,7 @@ add_subdirectory(goto-instrument)
 add_subdirectory(cpp)
 add_subdirectory(cbmc-concurrency)
 add_subdirectory(cbmc-cover)
+add_subdirectory(cbmc-incr-oneloop)
 add_subdirectory(goto-instrument-typedef)
 add_subdirectory(smt2_solver)
 add_subdirectory(smt2_strings)

regression/Makefile

@@ -9,6 +9,7 @@ DIRS = cbmc \
        cpp \
        cbmc-concurrency \
        cbmc-cover \
+       cbmc-incr-oneloop \
        goto-instrument-typedef \
        smt2_solver \
        smt2_strings \

regression/cbmc-incr-oneloop/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "perl -e 'alarm shift @ARGV; exec @ARGV' 8 $<TARGET_FILE:cbmc> --slice-formula"
+)

regression/cbmc-incr-oneloop/Makefile

@@ -1,10 +1,11 @@
 default: tests.log
 
+# Note the `perl -e` serves the purpose of providing timeout
 test:
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula"
+	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"
 
 tests.log: ../test.pl
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula"
+	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"
 
 show:
 	@for dir in *; do \