Skip to content

Commit

Permalink
cbmc-concurrency tests: FreeBSD would require sound pointer handling
Browse files Browse the repository at this point in the history
This is the same problem as previously seen on macOS.
  • Loading branch information
tautschnig committed Oct 13, 2023
1 parent 6ae4e26 commit bf49881
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion regression/cbmc-concurrency/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
if((NOT WIN32) AND (NOT APPLE))
if((NOT WIN32) AND (NOT APPLE) AND (NOT (CMAKE_SYSTEM_NAME STREQUAL "FreeBSD")))
add_test_pl_tests(
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
)
Expand Down
4 changes: 2 additions & 2 deletions regression/cbmc-concurrency/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ default: tests.log
include ../../src/config.inc
include ../../src/common

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

Expand Down

0 comments on commit bf49881

Please sign in to comment.