Merge pull request #7848 from tautschnig/bugfixes/c++-bitfields

C++ front-end: fix type checking of anonymous bit fields

Author: kroening

regression/ansi-c/CMakeLists.txt

@@ -7,15 +7,10 @@ elseif("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
         "$<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"
+        "-C;-I;test-c++-front-end;-s;c++-front-end"
         "CORE"
     )
 else()

regression/ansi-c/Makefile

@@ -11,15 +11,6 @@ endif
 
 ifeq ($(BUILD_ENV_),MSVC)
 	excluded_tests = -X gcc-only -X clang-only
-else
-ifeq ($(BUILD_ENV_),OSX)
-	# 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.
-  excluded_tests = -X macos-assert-broken
-endif
 endif
 
 test:

regression/ansi-c/array_initialization2/test.desc

@@ -1,4 +1,4 @@
-CORE test-c++-front-end macos-assert-broken
+CORE test-c++-front-end
 main.c
 
 ^EXIT=0$

regression/ansi-c/float_constant2/test.desc

@@ -1,4 +1,4 @@
-CORE test-c++-front-end macos-assert-broken
+CORE test-c++-front-end
 main.c
 
 ^EXIT=0$

regression/ansi-c/goto_convert_switch_range_case_valid/test.desc

@@ -1,4 +1,4 @@
-CORE test-c++-front-end macos-assert-broken
+CORE test-c++-front-end
 main.c
 
 ^EXIT=0$

regression/cbmc-cpp/Address_of_Method1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG macos-assert-broken
+KNOWNBUG
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Anonymous_members1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Assignment1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/CMakeLists.txt

@@ -4,12 +4,6 @@ else()
   set(gcc_only "")
 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_mac_broken_tests}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only}
 )

regression/cbmc-cpp/Class_Members1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Comma_Operator1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/ConditionalExpression1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/ConditionalExpression2/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Constructor1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Constructor12/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Constructor13/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Constructor2/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Constructor3/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Constructor4/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Constructor5/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Constructor6/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Constructor9/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Conversion5/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Conversion6/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Conversion_Operator2/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Conversion_Operator3/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Conversion_Operator4/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Default_Arguments1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Default_Arguments2/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Destructor_with_PtrMember/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Float1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Friend5/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/FunctionParam1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Function_Arguments2/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Function_Arguments5/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Function_Pointer1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Implicit_Conversion1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Implicit_Conversion4/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Implicit_Conversion6/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Implicit_Conversion7/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Inheritance1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Inheritance3/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Inheritance4/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Initializer1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Label0/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Linking1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 module.cpp
 ^EXIT=0$

regression/cbmc-cpp/Makefile

@@ -5,15 +5,6 @@ include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
 	excluded_tests = -X gcc-only
-else
-ifeq ($(BUILD_ENV_),OSX)
-	# 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.
-  excluded_tests = -X macos-assert-broken
-endif
 endif
 
 test:

regression/cbmc-cpp/Member_Access_in_Class/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/MethodParam1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 instance is SATISFIABLE$

regression/cbmc-cpp/Mutable1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Overloading_Functions1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Overloading_Functions3/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Overloading_Increment1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Overloading_Members1/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Overloading_Operators12/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Overloading_Operators13/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Overloading_Operators2/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Overloading_Operators7/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG macos-assert-broken
+KNOWNBUG
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Overloading_Operators8/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$

regression/cbmc-cpp/Pointer_Conversion2/test.desc

@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$