Merge pull request #7857 from tautschnig/cleanup/no-winbug

Purge winbug from regression tests

Author: kroening

regression/README.md

@@ -25,11 +25,3 @@ This folder contains the CProver regression test-suite.
   These tests are known to not work with Z3 (the version running on our CI).
 - `thorough-z3-smt-backend`:
   These tests are too slow to be run in CI with Z3.
-
-### Platform
-
-- `winbug`:
-  These tests are currently known to be failing on Windows,
-  but passing on other platforms. https://github.com/diffblue/cbmc/pull/5572
-  will address one part thereof; the remaining ones are C++ tests that fail on
-  both Windows and MacOS for our lack of C++-11 support.

regression/book-examples/CMakeLists.txt

@@ -1,32 +1,26 @@
 if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
   set(gcc_only -X gcc-only)
-  set(gcc_only_string "-X;gcc-only;")
-  set(exclude_win_broken_tests -X winbug)
-  # We add the string at the end of the exclusion list, so it must not
-  # have the `;` at the end or it bugs out.
-  set(exclude_win_broken_tests_string "-X;winbug")
+  set(gcc_only_string "-X;gcc-only")
 else()
   set(gcc_only "")
   set(gcc_only_string "")
-  set(exclude_win_broken_tests "")
-  set(exclude_win_broken_tests_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(
     "book-examples-paths-lifo"
     "$<TARGET_FILE:cbmc> --paths lifo"
-    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}"
+    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo"
     "CORE"
 )
 
 add_test_pl_profile(
     "book-examples-cprover-smt2"
     "$<TARGET_FILE:cbmc> --cprover-smt2"
-    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
+    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2"
     "CORE"
 )
 

regression/cbmc/CMakeLists.txt

@@ -1,32 +1,26 @@
 if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
   set(gcc_only -X gcc-only)
   set(gcc_only_string "-X;gcc-only;")
-  set(exclude_win_broken_tests -X winbug)
-  # We add the string at the end of the exclusion list, so it must not
-  # have the `;` at the end or it bugs out.
-  set(exclude_win_broken_tests_string "-X;winbug")
 else()
   set(gcc_only "")
   set(gcc_only_string "")
-  set(exclude_win_broken_tests "")
-  set(exclude_win_broken_tests_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;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}"
+    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo"
     "CORE"
 )
 
 add_test_pl_profile(
     "cbmc-cprover-smt2"
     "$<TARGET_FILE:cbmc> --cprover-smt2"
-    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
+    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2"
     "CORE"
 )
 

regression/cbmc/export-symex-ready-goto/test-bad-usage.desc

@@ -8,8 +8,3 @@ test.c
 --
 Ensure that --export-symex-ready-goto exported.symex-ready.goto terminates
 with error when incorrectly used.
-
-The reason why we use `winbug` is that it fails on certain windows system
-probably due to different interpretation of "". Not a bug, but we're using
-that label to remain consistent with other parts of the codebase, and not
-to unnecessarily introduce new ones for simple use cases.