Skip to content

Commit c954ba7

Browse files
committed
fixup! goto-symex/concurrency: limit unsoundness-abort to dereferencing shared pointers
1 parent 60e210f commit c954ba7

File tree

2 files changed

+2
-3
lines changed

2 files changed

+2
-3
lines changed

regression/cbmc-concurrency/CMakeLists.txt

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

regression/cbmc-concurrency/Makefile

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,8 @@ default: tests.log
33
include ../../src/config.inc
44
include ../../src/common
55

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

0 commit comments

Comments
 (0)