Run CBMC regression tests with --paths lifo in CI

We were not regularly exercising this code outside unit tests, leading to
regressions on several tests. On my system, running this additional test takes
42 seconds, which is still better than users running into issues. (ctest -V -L
CORE -j8 takes an extra 10 seconds.)

Fixes: diffblue#3956

Author: tautschnig

.travis.yml

@@ -358,6 +358,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>" -X smt-backend
 )
+
+add_test_pl_profile(
+    "cbmc-paths-lifo"
+    "$<TARGET_FILE:cbmc> --paths lifo"
+    "-C;-X;thorough-paths;-s;paths-lifo"
+    "CORE"
+)

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
+
 tests.log: ../test.pl
 	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
 

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$