Deactivate three broken tests on MacOS.

NlightNFotis · NlightNFotis · commit 30888f22b400 · 2020-11-03T11:42:54.000Z
The reason we are deactivating the tests is that there
was a change to the `assert.h` header under MacOS that
makes it now include some other C++ headers which include
`type_traits` causing template errors that have broken
CI under that platform.
diff --git a/regression/ansi-c/CMakeLists.txt b/regression/ansi-c/CMakeLists.txt
@@ -1,15 +1,20 @@
 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>" -X macos-assert-broken
+    )
 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
@@ -9,16 +9,22 @@ else
 	exe=../../../src/goto-cc/goto-cc
 endif
 
+ifeq ($(OS), Darwin)
+	exclude_mac_broken_tests = -X macos-assert-broken
+else
+	exclude_mac_broken_tests = 
+endif
+
 test:
-	@../test.pl -e -p -c $(exe)
+	@../test.pl -e -p -c $(exe) $(exclude_mac_broken_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 $(exclude_mac_broken_tests)
 endif
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c $(exe)
+	@../test.pl -e -p -c $(exe) $(exclude_mac_broken_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 $(exclude_mac_broken_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
@@ -9,11 +9,17 @@ else
 	gcc_only =
 endif
 
+ifeq ($(OS), Darwin)
+	exclude_mac_broken_tests = -X macos-assert-broken
+else
+	exclude_mac_broken_tests = 
+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" $(gcc_only) $(exclude_mac_broken_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" $(gcc_only) $(exclude_mac_broken_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
@@ -9,11 +9,17 @@ else
 	exe=../../../src/goto-cc/goto-cc
 endif
 
+ifeq ($(OS), Darwin)
+	exclude_mac_broken_tests = -X macos-assert-broken
+else
+	exclude_mac_broken_tests = 
+endif
+
 test:
-	@../test.pl -e -p -c $(exe)
+	@../test.pl -e -p -c $(exe) $(exclude_mac_broken_tests)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c $(exe)
+	@../test.pl -e -p -c $(exe) $(exclude_mac_broken_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,16 @@
+ifeq ($(OS), Darwin)
+	exclude_mac_broken_tests = -X macos-assert-broken
+else
+	exclude_mac_broken_tests = 
+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" $(exclude_mac_broken_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" $(exclude_mac_broken_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$

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE test-c++-front-end`
	`1`	`+CORE test-c++-front-end macos-assert-broken`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+CORE macos-assert-broken`
`2`	`2`	`main.cpp`
`3`	`3`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE winbug`
	`1`	`+CORE winbug macos-assert-broken`
`2`	`2`	`main.cpp`
`3`	`3`	`--pointer-check`
`4`	`4`	`^EXIT=0$`