File tree Expand file tree Collapse file tree 20 files changed +69
-34
lines changed
goto_convert_switch_range_case_valid Expand file tree Collapse file tree 20 files changed +69
-34
lines changed Original file line number Diff line number Diff line change 1
1
if ("${CMAKE_CXX_COMPILER_ID} " STREQUAL "MSVC" )
2
- add_test_pl_tests (
3
- "$<TARGET_FILE:goto-cc>" -X gcc-only
4
- )
2
+ add_test_pl_tests (
3
+ "$<TARGET_FILE:goto-cc>" -X gcc-only
4
+ )
5
+ elseif ("${CMAKE_SYSTEM_NAME} " STREQUAL "Darwin" )
6
+ add_test_pl_tests (
7
+ "$<TARGET_FILE:goto-cc>" -X macos-assert-broken
8
+ )
5
9
else ()
6
- add_test_pl_tests (
7
- "$<TARGET_FILE:goto-cc>"
8
- )
9
- add_test_pl_profile (
10
- "ansi-c-c++-front-end"
11
- "$<TARGET_FILE:goto-cc> -xc++ -D_Bool=bool"
12
- "-C;-I;test-c++-front-end;-s;c++-front-end"
13
- "CORE"
14
- )
10
+ add_test_pl_tests (
11
+ "$<TARGET_FILE:goto-cc>"
12
+ )
13
+
14
+ add_test_pl_profile (
15
+ "ansi-c-c++-front-end"
16
+ "$<TARGET_FILE:goto-cc> -xc++ -D_Bool=bool"
17
+ "-C;-I;test-c++-front-end;-s;c++-front-end"
18
+ "CORE"
19
+ )
15
20
endif ()
Original file line number Diff line number Diff line change 9
9
exe=../../../src/goto-cc/goto-cc
10
10
endif
11
11
12
+ ifeq ($(OS ) , Darwin)
13
+ exclude_mac_broken_tests = -X macos-assert-broken
14
+ else
15
+ exclude_mac_broken_tests =
16
+ endif
17
+
12
18
test :
13
19
@../test.pl -e -p -c $(exe )
14
20
ifneq ($(BUILD_ENV_ ) ,MSVC)
15
- @../test.pl -e -p -c "$(exe) -xc++ -D_Bool=bool" -I test-c++-front-end -s c++-front-end
21
+ @../test.pl -e -p -c "$(exe) -xc++ -D_Bool=bool" -I test-c++-front-end -s c++-front-end $(exclude_mac_broken_tests)
16
22
endif
17
23
18
24
tests.log : ../test.pl
19
25
@../test.pl -e -p -c $(exe )
20
26
ifneq ($(BUILD_ENV_ ) ,MSVC)
21
- @../test.pl -e -p -c "$(exe) -xc++ -D_Bool=bool" -I test-c++-front-end -s c++-front-end
27
+ @../test.pl -e -p -c "$(exe) -xc++ -D_Bool=bool" -I test-c++-front-end -s c++-front-end $(exclude_mac_broken_tests)
22
28
endif
23
29
24
30
show :
Original file line number Diff line number Diff line change 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
- 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
- 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 @@ -10,6 +10,12 @@ else()
10
10
set (exclude_win_broken_tests "" )
11
11
endif ()
12
12
13
+ if ("${CMAKE_SYSTEM_NAME} " STREQUAL "Darwin" )
14
+ set (exclude_mac_broken_tests -X macos-assert-broken )
15
+ else ()
16
+ set (exclude_mac_broken_tests "" )
17
+ endif ()
18
+
13
19
add_test_pl_tests (
14
- "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only} ${exclude_win_broken_tests}
20
+ "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only} ${exclude_win_broken_tests} ${exclude_mac_broken_tests}
15
21
)
Original file line number Diff line number Diff line change 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 9
9
gcc_only =
10
10
endif
11
11
12
+ ifeq ($(OS ) , Darwin)
13
+ exclude_mac_broken_tests = -X macos-assert-broken
14
+ else
15
+ exclude_mac_broken_tests =
16
+ endif
17
+
12
18
test :
13
- @../test.pl -e -p -c " ../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only )
19
+ @../test.pl -e -p -c " ../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only ) $( exclude_mac_broken_tests )
14
20
15
21
tests.log : ../test.pl
16
- @../test.pl -e -p -c " ../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only )
22
+ @../test.pl -e -p -c " ../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only ) $( exclude_mac_broken_tests )
17
23
18
24
show :
19
25
@for dir in * ; do \
Original file line number Diff line number Diff line change 1
- CORE
1
+ CORE macos-assert-broken
2
2
main.cpp
3
3
4
4
instance is SATISFIABLE$
Original file line number Diff line number Diff line change 1
- CORE winbug
1
+ CORE winbug macos-assert-broken
2
2
main.cpp
3
3
--pointer-check
4
4
^EXIT=0$
You can’t perform that action at this time.
0 commit comments