Merge pull request #3976 from tautschnig/paths-regression-test

Run CBMC regression tests with --paths lifo in CI

Author: tautschnig

.travis.yml

@@ -303,6 +303,7 @@ install:
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
+  - UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-paths-lifo
   - scripts/delete_failing_smt2_solver_tests ; env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
   - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C unit test

buildspec-windows.yml

@@ -40,6 +40,10 @@ phases:
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test BUILD_ENV=MSVC" '
 
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/cbmc test-paths-lifo BUILD_ENV=MSVC" '
+
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test BUILD_ENV=MSVC" '

buildspec.yml

@@ -25,6 +25,7 @@ phases:
     commands:
       - make -C unit test
       - make -C regression test
+      - make -C regression/cbmc test-paths-lifo
       - scripts/delete_failing_smt2_solver_tests
       - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
       - make -C jbmc/unit test

regression/cbmc/CMakeLists.txt

@@ -1,3 +1,10 @@
 add_test_pl_tests(
     "$<TARGET_FILE:cbmc> --validate-goto-model" -X smt-backend
 )
+
+add_test_pl_profile(
+    "cbmc-paths-lifo"
+    "$<TARGET_FILE:cbmc> --paths lifo"
+    "-C;-X;thorough-paths;-X;smt-backend;-s;paths-lifo"
+    "CORE"
+)

regression/cbmc/Failing_Assert1/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^Runtime decision procedure: [0-9]+(\.[0-9]+)?s$
+^Runtime decision procedure: [0-9]+(\.[0-9]+(e-[0-9]+)?)?s$
 --
 ^warning: ignoring

regression/cbmc/Makefile

@@ -6,6 +6,9 @@ test:
 test-cprover-smt2:
 	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
 
+test-paths-lifo:
+	@../test.pl -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend
+
 tests.log: ../test.pl test
 
 show:

regression/cbmc/Multi_Dimensional_Array6/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
 main.c
 --unwind 3 --no-unwinding-assertions
 ^EXIT=10$

regression/cbmc/address_space_size_limit1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
 test.c
 --no-simplify --unwind 300 --object-bits 8
 too many addressed objects

regression/cbmc/array-tests/test.desc

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