Merge pull request #5573 from tautschnig/debug-winbug

Fix PATH separator and CMake syntax to make cbmc-cprover-smt2 tests work on Windows

Author: tautschnig

regression/cbmc/CMakeLists.txt

@@ -1,41 +1,40 @@
 if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
   set(gcc_only -X gcc-only)
+  set(gcc_only_string "-X;gcc-only;")
 else()
   set(gcc_only "")
-endif()
-
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  set(exclude_win_broken_tests -X winbug)
-else()
-  set(exclude_win_broken_tests "")
+  set(gcc_only_string "")
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_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"
-    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;-s;paths-lifo"
+    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo"
     "CORE"
-    ${gcc_only}
 )
 
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  message(WARNING "Tests are failing on windows under this config, for reasons unknown. Investigation is pending.")
-else()
-  add_test_pl_profile(
+add_test_pl_profile(
     "cbmc-cprover-smt2"
     "$<TARGET_FILE:cbmc> --cprover-smt2"
-    "-C;-X;broken-smt-backend;-s;cprover-smt2"
+    "-C;-X;broken-smt-backend;${gcc_only_string}-s;cprover-smt2"
     "CORE"
-    ${gcc_only}
-    )
+)
 
+if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+  set_property(
+    TEST "cbmc-cprover-smt2-CORE"
+    PROPERTY ENVIRONMENT
+      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
+  )
+else()
+  string(REPLACE ";" "\\;" path_value "$ENV{PATH}")
   set_property(
     TEST "cbmc-cprover-smt2-CORE"
     PROPERTY ENVIRONMENT
-      "PATH=$ENV{PATH}:${CMAKE_BINARY_DIR}/bin"
+      "PATH=${path_value}\;$<TARGET_FILE_DIR:smt2_solver>"
   )
 endif()

regression/cbmc/address_space_size_limit1/test.desc

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