Skip to content

Commit

Permalink
C++ front-end: fix type checking of anonymous bit fields
Browse files Browse the repository at this point in the history
For `unsigned x : 2, : 2;` we tried to merge a necessarily empty (not
nil!) irept via `merge_types`. MacOS has such anonymous bit fields in
some system headers.
  • Loading branch information
tautschnig committed Aug 16, 2023
1 parent fa1d719 commit be2a41c
Show file tree
Hide file tree
Showing 137 changed files with 133 additions and 191 deletions.
7 changes: 1 addition & 6 deletions regression/ansi-c/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
9 changes: 0 additions & 9 deletions regression/ansi-c/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion regression/ansi-c/array_initialization2/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE test-c++-front-end macos-assert-broken
CORE test-c++-front-end
main.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/ansi-c/float_constant2/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE test-c++-front-end macos-assert-broken
CORE test-c++-front-end
main.c

^EXIT=0$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE test-c++-front-end macos-assert-broken
CORE test-c++-front-end
main.c

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Address_of_Method1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG macos-assert-broken
KNOWNBUG
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Anonymous_members1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Assignment1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
8 changes: 1 addition & 7 deletions regression/cbmc-cpp/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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}
)
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Class_Members1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Comma_Operator1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/ConditionalExpression1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/ConditionalExpression2/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Constructor1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Constructor12/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Constructor13/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Constructor2/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Constructor3/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Constructor4/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Constructor5/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Constructor6/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Constructor9/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Conversion5/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Conversion6/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Conversion_Operator2/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Conversion_Operator3/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Conversion_Operator4/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Default_Arguments1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Default_Arguments2/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Destructor_with_PtrMember/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Float1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Friend5/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/FunctionParam1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Function_Arguments2/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Function_Arguments5/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Function_Pointer1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Implicit_Conversion1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Implicit_Conversion4/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Implicit_Conversion6/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Implicit_Conversion7/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Inheritance1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Inheritance3/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Inheritance4/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Initializer1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Label0/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Linking1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp
module.cpp
^EXIT=0$
Expand Down
9 changes: 0 additions & 9 deletions regression/cbmc-cpp/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Member_Access_in_Class/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/MethodParam1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

instance is SATISFIABLE$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Mutable1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Overloading_Functions1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Overloading_Functions3/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Overloading_Increment1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Overloading_Members1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Overloading_Operators12/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Overloading_Operators13/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Overloading_Operators2/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Overloading_Operators7/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG macos-assert-broken
KNOWNBUG
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Overloading_Operators8/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cpp/Pointer_Conversion2/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
CORE macos-assert-broken
CORE
main.cpp

^EXIT=0$
Expand Down
Loading

0 comments on commit be2a41c

Please sign in to comment.