Skip to content

Commit 1a96b1c

Browse files
committed
cbmc-concurrency tests: FreeBSD would require sound pointer handling
This is the same problem as previously seen on macOS.
1 parent 63faa7f commit 1a96b1c

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

regression/cbmc-concurrency/CMakeLists.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
if((NOT WIN32) AND (NOT APPLE))
1+
if((NOT WIN32) AND (NOT APPLE) AND (NOT (CMAKE_SYSTEM_NAME STREQUAL "FreeBSD")))
22
add_test_pl_tests(
33
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
44
)

regression/cbmc-concurrency/Makefile

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ default: tests.log
33
include ../../src/config.inc
44
include ../../src/common
55

6-
ifeq ($(filter-out OSX MSVC,$(BUILD_ENV_)),)
6+
ifeq ($(filter-out OSX MSVC FreeBSD,$(BUILD_ENV_)),)
77
# no POSIX threads on Windows
8-
# for OSX we'd need sound handling of pointers in multi-threaded programs
8+
# for OSX and FreeBSD we'd need sound handling of pointers in multi-threaded programs
99
no_pthread = -X pthread
1010
endif
1111

0 commit comments

Comments
 (0)