diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt index 4397b08193d..9df03762567 100644 --- a/regression/cbmc/CMakeLists.txt +++ b/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( - "$ --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests} + "$ --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ) add_test_pl_profile( "cbmc-paths-lifo" "$ --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" "$ --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}:$" + ) +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}\;$" ) endif() diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc index 58096c85232..3bc849b0cbf 100644 --- a/regression/cbmc/address_space_size_limit1/test.desc +++ b/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