Skip to content

Commit fa1d719

Browse files
authored
Merge pull request #7849 from tautschnig/cleanup/winbug
Remove avoidable use of winbug test exclusion
2 parents 8035d4a + c9afc1e commit fa1d719

File tree

138 files changed

+143
-184
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

138 files changed

+143
-184
lines changed

regression/cbmc-cpp/Address_of_Method1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG winbug macos-assert-broken
1+
KNOWNBUG macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Anonymous_members1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Assignment1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/CMakeLists.txt

+1-7
Original file line numberDiff line numberDiff line change
@@ -4,18 +4,12 @@ else()
44
set(gcc_only "")
55
endif()
66

7-
if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
8-
set(exclude_win_broken_tests -X winbug)
9-
else()
10-
set(exclude_win_broken_tests "")
11-
endif()
12-
137
if("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
148
set(exclude_mac_broken_tests -X macos-assert-broken)
159
else()
1610
set(exclude_mac_broken_tests "")
1711
endif()
1812

1913
add_test_pl_tests(
20-
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only} ${exclude_win_broken_tests} ${exclude_mac_broken_tests}
14+
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only} ${exclude_mac_broken_tests}
2115
)

regression/cbmc-cpp/Class_Members1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Comma_Operator1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/ConditionalExpression1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/ConditionalExpression2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Constructor1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Constructor12/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Constructor13/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Constructor2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Constructor3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Constructor4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Constructor5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Constructor6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Constructor9/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Conversion5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Conversion6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Conversion_Operator2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Conversion_Operator3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Conversion_Operator4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Default_Arguments1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Default_Arguments2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Destructor_with_PtrMember/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Float1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Friend5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Function_Arguments2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Function_Arguments5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Function_Pointer1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Implicit_Conversion1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Implicit_Conversion4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Implicit_Conversion6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Implicit_Conversion7/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Inheritance1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Inheritance3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Inheritance4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Initializer1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Label0/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Linking1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33
module.cpp
44
^EXIT=0$

regression/cbmc-cpp/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ include ../../src/config.inc
44
include ../../src/common
55

66
ifeq ($(BUILD_ENV_),MSVC)
7-
excluded_tests = -X gcc-only -X winbug
7+
excluded_tests = -X gcc-only
88
else
99
ifeq ($(BUILD_ENV_),OSX)
1010
# In MacOS, a change in the assert.h header file

regression/cbmc-cpp/Member_Access_in_Class/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Mutable1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Overloading_Functions1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Overloading_Functions3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Overloading_Increment1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Overloading_Members1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Overloading_Operators12/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Overloading_Operators13/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Overloading_Operators2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Overloading_Operators7/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG winbug macos-assert-broken
1+
KNOWNBUG macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Overloading_Operators8/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Pointer_Conversion2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Protection2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Qualifier2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Reference2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Reference3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Reference6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Reference7/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Resolver6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Resolver7/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Resolver8/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

regression/cbmc-cpp/Static_Method1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE winbug macos-assert-broken
1+
CORE macos-assert-broken
22
main.cpp
33

44
^EXIT=0$

0 commit comments

Comments
 (0)