Skip to content

Commit ff6080c

Browse files
committed
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.
1 parent 55362f6 commit ff6080c

File tree

11 files changed

+19
-13
lines changed

11 files changed

+19
-13
lines changed

regression/cbmc-sequentialization/CMakeLists.txt

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,30 @@
1+
if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
2+
set(exclude_windows_unsupported_tests -X requires_posix_only_headers)
3+
else()
4+
set(exclude_windows_unsupported_tests "")
5+
endif()
6+
17
if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
28
set(gcc_only -X gcc-only)
39
else()
410
set(gcc_only "")
511
endif()
612

713
add_test_pl_tests(
8-
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only}
14+
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_windows_unsupported_tests}
915
)
1016

1117
add_test_pl_profile(
1218
"cbmc-paths-lifo"
1319
"$<TARGET_FILE:cbmc> --paths lifo"
14-
"-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;-s;paths-lifo ${gcc_only}"
20+
"-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;-s;paths-lifo ${gcc_only} ${exclude_windows_unsupported_tests}"
1521
"CORE"
1622
)
1723

1824
add_test_pl_profile(
1925
"cbmc-cprover-smt2"
2026
"$<TARGET_FILE:cbmc> --cprover-smt2"
21-
"-C;-X;broken-smt-backend;-s;cprover-smt2 ${gcc_only}"
27+
"-C;-X;broken-smt-backend;-s;cprover-smt2 ${gcc_only} ${exclude_windows_unsupported_tests}"
2228
"CORE"
2329
)
2430

regression/cbmc-sequentialization/posix_semaphores/blocking_queue.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
FUTURE requires_posix_only_headers
22
blocking_queue.c
33

44
^EXIT=0$

regression/cbmc-sequentialization/posix_semaphores/blocking_wait.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
FUTURE requires_posix_only_headers
22
blocking_wait.c
33

44
^EXIT=0$

regression/cbmc-sequentialization/posix_semaphores/create_destroy.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE requires_posix_only_headers
22
create_destroy.c
33

44
^EXIT=0$

regression/cbmc-sequentialization/pthread_cond/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
FUTURE requires_posix_only_headers
22
test.c
33

44
^EXIT=0$

regression/cbmc-sequentialization/pthread_join/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
FUTURE requires_posix_only_headers
22
main.c
33

44
^EXIT=0$

regression/cbmc-sequentialization/pthread_mutex/no_mutex.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
FUTURE requires_posix_only_headers
22
no_mutex.c
33

44
^EXIT=0$

regression/cbmc-sequentialization/pthread_mutex/with_mutex.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
FUTURE requires_posix_only_headers
22
with_mutex.c
33

44
^EXIT=0$

regression/cbmc-sequentialization/pthread_self_equal/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
FUTURE requires_posix_only_headers
22
main.c
33

44
^EXIT=0$

regression/cbmc-sequentialization/rw_lock/race_test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
FUTURE requires_posix_only_headers
22
with_lock.c
33
--unwind 10
44
^EXIT=0$

regression/cbmc-sequentialization/rw_lock/with_lock.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
FUTURE requires_posix_only_headers
22
with_lock.c
33
--unwind 10
44
^EXIT=0$

0 commit comments

Comments
 (0)