Merge pull request #5938 from tautschnig/k-induction-tests

Enable regression tests of k-induction instrumentation

Author: kroening

regression/CMakeLists.txt

@@ -53,6 +53,7 @@ add_subdirectory(statement-list)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(acceleration)
+add_subdirectory(k-induction)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-harness-multi-file-project)
 add_subdirectory(goto-cc-file-local)

regression/Makefile

@@ -28,6 +28,7 @@ DIRS = cbmc \
        systemc \
        contracts \
        acceleration \
+       k-induction \
        goto-harness \
        goto-harness-multi-file-project \
        goto-cc-file-local \

regression/k-induction/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
+)

regression/k-induction/Makefile

@@ -1,10 +1,21 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
 test:
-	@../test.pl -c ../chain.sh
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
 
-tests.log: ../test.pl
-	@../test.pl -c ../chain.sh
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
 
 show:
 	@for dir in *; do \

regression/k-induction/chain.sh

@@ -2,10 +2,12 @@
 
 set -e
 
-src=../../../src
-goto_cc=$src/goto-cc/goto-cc
-goto_instrument=$src/goto-instrument/goto-instrument
-cbmc=$src/cbmc/cbmc
+goto_cc=$1
+goto_instrument=$2
+cbmc=$3
+is_windows=$4
+
+shift 4
 
 function usage() {
   echo "Usage: chain k test_file.c"
@@ -15,10 +17,23 @@ function usage() {
 name=`echo $2 | cut -d. -f1`
 k=$1
 
-$goto_cc -o $name.o $name.c
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "${name}.c" "/Fe${name}.gb"
+else
+  $goto_cc -o "${name}.gb" "${name}.c"
+fi
+
 
-$goto_instrument --k-induction $k --base-case $name.o $name.base.o
-if $cbmc $name.base.o ; then echo "## Base case passes" ; else echo "## Base case fails" ; fi
+"$goto_instrument" --k-induction $k --base-case "$name.gb" "$name.base.gb"
+if "$cbmc" "$name.base.gb" ; then
+  echo "## Base case passes"
+else
+  echo "## Base case fails"
+fi
 
-$goto_instrument --k-induction $k --step-case $name.o $name.step.o
-if $cbmc $name.step.o ; then echo "## Step case passes" ; else echo "## Step case fails" ; fi
+"$goto_instrument" --k-induction $k --step-case "$name.gb" "$name.step.gb"
+if "$cbmc" "$name.step.gb" ; then
+  echo "## Step case passes"
+else
+  echo "## Step case fails"
+fi