File tree Expand file tree Collapse file tree 4 files changed +7
-17
lines changed
cbmc/export-symex-ready-goto Expand file tree Collapse file tree 4 files changed +7
-17
lines changed Original file line number Diff line number Diff line change 1- CORE winbug
1+ CORE
22test.c
3- --export-symex-ready-goto ""
3+ --export-symex-ready-goto ''
44^ERROR: Please provide a filename to write the goto-binary to.$
55^EXIT=6$
66^SIGNAL=0$
Original file line number Diff line number Diff line change 11if ("${CMAKE_SYSTEM_NAME} " STREQUAL "Windows" )
22 set (is_windows true )
3- set (exclude_win_broken_tests -X winbug)
43else ()
54 set (is_windows false )
6- set (exclude_win_broken_tests "" )
75endif ()
86
97add_test_pl_tests(
10- "${CMAKE_CURRENT_SOURCE_DIR} /chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-inspect> ${is_windows} " ${exclude_win_broken_tests}
8+ "${CMAKE_CURRENT_SOURCE_DIR} /chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-inspect> ${is_windows} "
119)
Original file line number Diff line number Diff line change @@ -6,17 +6,16 @@ include ../../src/common
66ifeq ($(BUILD_ENV_ ) ,MSVC)
77 exe=../../../src/goto-cc/goto-cl
88 is_windows=true
9- excluded_tests = -X winbug
109else
1110 exe=../../../src/goto-cc/goto-cc
1211 is_windows=false
1312endif
1413
1514test :
16- @../test.pl -e -p -c ' ../chain.sh $(exe) ../../../src/goto-inspect/goto-inspect $(is_windows)' $( excluded_tests )
15+ @../test.pl -e -p -c ' ../chain.sh $(exe) ../../../src/goto-inspect/goto-inspect $(is_windows)'
1716
1817tests.log :
19- @../test.pl -e -p -c ' ../chain.sh $(exe) ../../../src/goto-inspect/goto-inspect $(is_windows)' $( excluded_tests )
18+ @../test.pl -e -p -c ' ../chain.sh $(exe) ../../../src/goto-inspect/goto-inspect $(is_windows)'
2019
2120clean :
2221 find . -name ' *.out' -execdir $(RM ) ' {}' \;
Original file line number Diff line number Diff line change 1- CORE winbug
1+ CORE
22main.c
3- " "
3+ ' '
44^EXIT=6$
55^SIGNAL=0$
66--
@@ -13,10 +13,3 @@ END_FUNCTION
1313--
1414This is testing the behaviour of the goto-inspect binary in case a binary
1515is present, but no inspection option is present.
16-
17- This is labelled `winbug` to avoid running on windows because of issues with
18- the empty string in line 3 (simulating the lack of an option) not working as
19- it should (it is contrary to the behaviour of unix systems). The behaviour
20- has been verified manually on a machine as working as expected, but getting
21- the test to run automatically is a lot more involved, so we're opting to
22- skipping this on that platform for now.
You can’t perform that action at this time.
0 commit comments