diffblue · NlightNFotis · Nov 6, 2020 · Nov 2, 2020
diff --git a/regression/ansi-c/CMakeLists.txt b/regression/ansi-c/CMakeLists.txt
@@ -1,15 +1,32 @@
 if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
-add_test_pl_tests(
-    "$<TARGET_FILE:goto-cc>" -X gcc-only
-)
+    add_test_pl_tests(
+        "$<TARGET_FILE:goto-cc>" -X gcc-only
+    )
+elseif("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
+    add_test_pl_tests(
+        "$<TARGET_FILE:goto-cc>"
+    )
+
+    # In MacOS, a change in the assert.h header file
+    # is causing template errors when exercising the
+    # C++ front end (because of a transitive include
+    # of <type_traits>) for files that include the
+    # <assert.h> or <cassert> headers.
+    add_test_pl_profile(
+        "ansi-c-c++-front-end"
+        "$<TARGET_FILE:goto-cc> -xc++ -D_Bool=bool"
+        "-C;-I;test-c++-front-end;-s;c++-front-end-X;macos-assert-broken"
+        "CORE"
+    )
 else()
-add_test_pl_tests(
-    "$<TARGET_FILE:goto-cc>"
-)
-add_test_pl_profile(
-    "ansi-c-c++-front-end"
-    "$<TARGET_FILE:goto-cc> -xc++ -D_Bool=bool"
-    "-C;-I;test-c++-front-end;-s;c++-front-end"
-    "CORE"
-)
+    add_test_pl_tests(
+        "$<TARGET_FILE:goto-cc>"
+    )
+
+    add_test_pl_profile(
+        "ansi-c-c++-front-end"
+        "$<TARGET_FILE:goto-cc> -xc++ -D_Bool=bool"
+        "-C;-I;test-c++-front-end;-s;c++-front-end"
+        "CORE"
+    )
 endif()
diff --git a/regression/ansi-c/Makefile b/regression/ansi-c/Makefile
@@ -4,21 +4,35 @@ include ../../src/config.inc
 include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
-	exe=../../../src/goto-cc/goto-cl -X gcc-only
+	exe = ../../../src/goto-cc/goto-cl
 else
-	exe=../../../src/goto-cc/goto-cc
+	exe = ../../../src/goto-cc/goto-cc
+endif
+
+ifeq ($(BUILD_ENV_),MSVC)
+	excluded_tests = -X gcc-only
+else
+	# In MacOS, a change in the assert.h header file
+	# is causing template errors when exercising the
+	# C++ front end (because of a transitive include
+	# of <type_traits>) for files that include the
+	# <assert.h> or <cassert> headers.
+	OS := $(shell uname)
+	ifeq ($(OS),Darwin)
+		excluded_tests = -X macos-assert-broken
+	endif
 endif
 
 test:
-	@../test.pl -e -p -c $(exe)
+	@../test.pl -e -p -c $(exe) $(excluded_tests)
 ifneq ($(BUILD_ENV_),MSVC)
-	@../test.pl -e -p -c "$(exe) -xc++ -D_Bool=bool" -I test-c++-front-end -s c++-front-end
+	@../test.pl -e -p -c "$(exe) -xc++ -D_Bool=bool" -I test-c++-front-end -s c++-front-end $(excluded_tests)
 endif
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c $(exe)
+	@../test.pl -e -p -c $(exe) $(excluded_tests)
 ifneq ($(BUILD_ENV_),MSVC)
-	@../test.pl -e -p -c "$(exe) -xc++ -D_Bool=bool" -I test-c++-front-end -s c++-front-end
+	@../test.pl -e -p -c "$(exe) -xc++ -D_Bool=bool" -I test-c++-front-end -s c++-front-end $(excluded_tests)
 endif
 
 show:

diff --git a/regression/ansi-c/array_initialization2/test.desc b/regression/ansi-c/array_initialization2/test.desc
@@ -1,4 +1,4 @@
-CORE test-c++-front-end
+CORE test-c++-front-end macos-assert-broken
 main.c
 
 ^EXIT=0$

diff --git a/regression/ansi-c/float_constant2/test.desc b/regression/ansi-c/float_constant2/test.desc
@@ -1,4 +1,4 @@
-CORE test-c++-front-end
+CORE test-c++-front-end macos-assert-broken
 main.c
 
 ^EXIT=0$

diff --git a/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc b/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
@@ -1,4 +1,4 @@
-CORE test-c++-front-end
+CORE test-c++-front-end macos-assert-broken
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc-cpp/CMakeLists.txt b/regression/cbmc-cpp/CMakeLists.txt
@@ -10,6 +10,12 @@ else()
   set(exclude_win_broken_tests "")
 endif()
 
+if("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
+  set(exclude_mac_broken_tests -X macos-assert-broken)
+else()
+  set(exclude_mac_broken_tests "")
+endif()
+
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only} ${exclude_win_broken_tests}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only} ${exclude_win_broken_tests} ${exclude_mac_broken_tests}
 )
diff --git a/regression/cbmc-cpp/FunctionParam1/test.desc b/regression/cbmc-cpp/FunctionParam1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/cbmc-cpp/Makefile b/regression/cbmc-cpp/Makefile
@@ -4,16 +4,24 @@ include ../../src/config.inc
 include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
-	gcc_only = -X gcc-only
+	excluded_tests = -X gcc-only
 else
-	gcc_only =
+	# In MacOS, a change in the assert.h header file
+	# is causing template errors when exercising the
+	# C++ front end (because of a transitive include
+	# of <type_traits>) for files that include the
+	# <assert.h> or <cassert> headers.
+	OS := $(shell uname)
+	ifeq ($(OS),Darwin)
+		excluded_tests = -X macos-assert-broken
+	endif
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests)
 
 show:
 	@for dir in *; do \

diff --git a/regression/cbmc-cpp/MethodParam1/test.desc b/regression/cbmc-cpp/MethodParam1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE macos-assert-broken
 main.cpp
 
 instance is SATISFIABLE$

diff --git a/regression/cbmc-cpp/cpp-new/test.desc b/regression/cbmc-cpp/cpp-new/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 --pointer-check
 ^EXIT=0$

diff --git a/regression/cbmc-cpp/cpp1/test.desc b/regression/cbmc-cpp/cpp1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 --unwind 1 --unwinding-assertions
 ^EXIT=0$

diff --git a/regression/cbmc-cpp/lvalue1/test.desc b/regression/cbmc-cpp/lvalue1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/cbmc-cpp/union2/test.desc b/regression/cbmc-cpp/union2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE macos-assert-broken
 main.cpp
 --little-endian
 ^EXIT=0$

diff --git a/regression/cpp/CMakeLists.txt b/regression/cpp/CMakeLists.txt
@@ -10,6 +10,12 @@ else()
   set(exclude_win_broken_tests "")
 endif()
 
+if("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
+  set(exclude_mac_broken_tests -X macos-assert-broken)
+else()
+  set(exclude_mac_broken_tests "")
+endif()
+
 add_test_pl_tests(
-    "$<TARGET_FILE:goto-cc>" ${gcc_only} ${exclude_win_broken_tests}
+    "$<TARGET_FILE:goto-cc>" ${gcc_only} ${exclude_win_broken_tests} ${exclude_mac_broken_tests}
 )
diff --git a/regression/cpp/Makefile b/regression/cpp/Makefile
@@ -4,16 +4,29 @@ include ../../src/config.inc
 include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
-	exe=../../../src/goto-cc/goto-cl -X gcc-only
+	exe = ../../../src/goto-cc/goto-cl
 else
-	exe=../../../src/goto-cc/goto-cc
+	exe = ../../../src/goto-cc/goto-cc
 endif
 
-test:
-	@../test.pl -e -p -c $(exe)
+ifeq ($(BUILD_ENV_),MSVC)
+	excluded_tests = -X gcc-only
+else
+	# In MacOS, a change in the assert.h header file
+	# is causing template errors when exercising the
+	# C++ front end (because of a transitive include
+	# of <type_traits>) for files that include the
+	# <assert.h> or <cassert> headers.
+	OS := $(shell uname)
+	ifeq ($(OS),Darwin)
+		excluded_tests = -X macos-assert-broken
+	endif
+endif
 
+test:
+	@../test.pl -e -p -c $(exe) $(excluded_tests)
 tests.log: ../test.pl
-	@../test.pl -e -p -c $(exe)
+	@../test.pl -e -p -c $(exe) $(excluded_tests)
 
 show:
 	@for dir in *; do \

diff --git a/regression/cpp/Method_qualifier1/test.desc b/regression/cpp/Method_qualifier1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/cpp/auto1/test.desc b/regression/cpp/auto1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 -std=c++11
 ^EXIT=0$

diff --git a/regression/cpp/enum5/test.desc b/regression/cpp/enum5/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/cpp/switch1/test.desc b/regression/cpp/switch1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/cpp/virtual1/test.desc b/regression/cpp/virtual1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/systemc/Array2/test.desc b/regression/systemc/Array2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$

diff --git a/regression/systemc/Array3/test.desc b/regression/systemc/Array3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$

diff --git a/regression/systemc/Array4/test.desc b/regression/systemc/Array4/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$

diff --git a/regression/systemc/BitvectorCpp1/test.desc b/regression/systemc/BitvectorCpp1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/systemc/BitvectorCpp2/test.desc b/regression/systemc/BitvectorCpp2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/systemc/BitvectorSc3/test.desc b/regression/systemc/BitvectorSc3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/systemc/CMakeLists.txt b/regression/systemc/CMakeLists.txt
@@ -4,6 +4,12 @@ else()
   set(exclude_win_broken_tests "")
 endif()
 
+if("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
+  set(exclude_mac_broken_tests -X macos-assert-broken)
+else()
+  set(exclude_mac_broken_tests "")
+endif()
+
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${exclude_win_broken_tests}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${exclude_win_broken_tests} ${exclude_mac_broken_tests}
 )
diff --git a/regression/systemc/ForwardDecl1/test.desc b/regression/systemc/ForwardDecl1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/systemc/Makefile b/regression/systemc/Makefile
@@ -1,10 +1,22 @@
+ifneq ($(BUILD_ENV_),MSVC)
+	# In MacOS, a change in the assert.h header file
+	# is causing template errors when exercising the
+	# C++ front end (because of a transitive include
+	# of <type_traits>) for files that include the
+	# <assert.h> or <cassert> headers.
+	OS := $(shell uname)
+	ifeq ($(OS),Darwin)
+		excluded_tests = -X macos-assert-broken
+	endif
+endif
+
 default: tests.log
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation"
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation"
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests)
 
 show:
 	@for dir in *; do \

diff --git a/regression/systemc/Masc1/test.desc b/regression/systemc/Masc1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/systemc/MascInst1/test.desc b/regression/systemc/MascInst1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/systemc/Reference1/test.desc b/regression/systemc/Reference1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/systemc/This1/test.desc b/regression/systemc/This1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 
 ^EXIT=0$

diff --git a/regression/systemc/Tuple1/test.desc b/regression/systemc/Tuple1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$

diff --git a/regression/systemc/Tuple2/test.desc b/regression/systemc/Tuple2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE winbug macos-assert-broken
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$