Do not run tests which require POSIX specific headers on windows

These tests are disabled on windows for the moment because they require
POSIX specific header files which are not natively available on Windows.
A windows POSIX compatability layer library could potentially be used to
enable them to be run on Windows. However the work to do so has not been
done.

Author: thomasspriggs

regression/cbmc-sequentialization/CMakeLists.txt

@@ -1,25 +1,33 @@
+if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+  set(exclude_windows_unsupported_tests -X requires_posix_only_headers)
+else()
+  set(exclude_windows_unsupported_tests "")
+endif()
+
 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}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_windows_unsupported_tests}
 )
 
 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 ${gcc_only}"
     "CORE"
+    ${exclude_windows_unsupported_tests}
 )
 
 add_test_pl_profile(
     "cbmc-cprover-smt2"
     "$<TARGET_FILE:cbmc> --cprover-smt2"
     "-C;-X;broken-smt-backend;-s;cprover-smt2 ${gcc_only}"
     "CORE"
+    ${exclude_windows_unsupported_tests}
 )
 
 set_property(

regression/cbmc-sequentialization/posix_semaphores/blocking_queue.desc

@@ -1,4 +1,4 @@
-FUTURE
+FUTURE requires_posix_only_headers
 blocking_queue.c
 
 ^EXIT=0$

regression/cbmc-sequentialization/posix_semaphores/blocking_wait.desc

@@ -1,4 +1,4 @@
-FUTURE
+FUTURE requires_posix_only_headers
 blocking_wait.c
 
 ^EXIT=0$

regression/cbmc-sequentialization/posix_semaphores/create_destroy.desc

@@ -1,4 +1,4 @@
-CORE
+CORE requires_posix_only_headers
 create_destroy.c
 
 ^EXIT=0$

regression/cbmc-sequentialization/pthread_cond/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+FUTURE requires_posix_only_headers
 test.c
 
 ^EXIT=0$

regression/cbmc-sequentialization/pthread_join/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+FUTURE requires_posix_only_headers
 main.c
 
 ^EXIT=0$

regression/cbmc-sequentialization/pthread_mutex/no_mutex.desc

@@ -1,4 +1,4 @@
-FUTURE
+FUTURE requires_posix_only_headers
 no_mutex.c
 
 ^EXIT=0$

regression/cbmc-sequentialization/pthread_mutex/with_mutex.desc

@@ -1,4 +1,4 @@
-FUTURE
+FUTURE requires_posix_only_headers
 with_mutex.c
 
 ^EXIT=0$

regression/cbmc-sequentialization/pthread_self_equal/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+FUTURE requires_posix_only_headers
 main.c
 
 ^EXIT=0$

regression/cbmc-sequentialization/rw_lock/race_test.desc

@@ -1,4 +1,4 @@
-FUTURE
+FUTURE requires_posix_only_headers
 with_lock.c
 --unwind 10
 ^EXIT=0$

regression/cbmc-sequentialization/rw_lock/with_lock.desc

@@ -1,4 +1,4 @@
-FUTURE
+FUTURE requires_posix_only_headers
 with_lock.c
 --unwind 10
 ^EXIT=0$