Add test directory for future sequentialization work

This directory of regression tests is for examples which we intend to
use for testing the future work on the analysis of concurrent programs
based on a sequentialization approach.

Author: thomasspriggs

regression/cbmc-sequentialization/CMakeLists.txt

@@ -0,0 +1,29 @@
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+  set(gcc_only "-X gcc-only")
+else()
+  set(gcc_only "")
+endif()
+
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only}
+)
+
+add_test_pl_profile(
+    "cbmc-paths-lifo"
+    "$<TARGET_FILE:cbmc> --paths lifo ${gcc_only}"
+    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;-s;paths-lifo"
+    "CORE"
+)
+
+add_test_pl_profile(
+    "cbmc-cprover-smt2"
+    "$<TARGET_FILE:cbmc> --cprover-smt2 ${gcc_only}"
+    "-C;-X;broken-smt-backend;-s;cprover-smt2"
+    "CORE"
+)
+
+set_property(
+  TEST "cbmc-cprover-smt2-CORE"
+  PROPERTY ENVIRONMENT
+    "PATH=$ENV{PATH}:${CMAKE_BINARY_DIR}/bin"
+)

regression/cbmc-sequentialization/Makefile

@@ -0,0 +1,33 @@
+default: test
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+GCC_ONLY = -X gcc-only
+else
+GCC_ONLY =
+endif
+
+test:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
+
+test-cprover-smt2:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend $(GCC_ONLY)
+
+test-paths-lifo:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend -X paths-lifo-expected-failure $(GCC_ONLY)
+
+tests.log: ../test.pl test
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.smt2' -execdir $(RM) '{}' \;
+	$(RM) tests.log