Skip to content

Commit 0ee4b03

Browse files
committed
Exclude tests under cbmc-incr-oneloop/
1 parent 2b97b47 commit 0ee4b03

File tree

8 files changed

+16
-8
lines changed

8 files changed

+16
-8
lines changed
Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
2+
set(exclude_win_broken_tests -X winbug)
3+
else()
4+
set(exclude_win_broken_tests "")
5+
endif()
6+
17
add_test_pl_tests(
2-
"perl ../timeout.pl 8 $<TARGET_FILE:cbmc> --slice-formula"
8+
"perl ../timeout.pl 8 $<TARGET_FILE:cbmc> --slice-formula" ${exclude_win_broken_tests}
39
)

regression/cbmc-incr-oneloop/alarm1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE winbug
22
main.c
33
--incremental-loop main.0 --unwind-max 15
44
activate-multi-line-match

regression/cbmc-incr-oneloop/alarm3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE winbug
22
main.c
33
--incremental-loop main.0 --unwind-max 15 --unwinding-assertions
44
^EXIT=10$

regression/cbmc-incr-oneloop/cruise1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE winbug
22
main.c
33
--incremental-loop main.0 --unwind-max 10
44
^EXIT=0$
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,11 @@
11
if(WIN32)
22
set(is_windows true)
3+
set(exclude_win_broken_tests -X winbug)
34
else()
45
set(is_windows false)
6+
set(exclude_win_broken_tests "")
57
endif()
68

79
add_test_pl_tests(
8-
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> $<TARGET_FILE:goto-instrument> ${is_windows}"
10+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> $<TARGET_FILE:goto-instrument> ${is_windows}" ${exclude_win_broken_tests}
911
)

regression/goto-cc-instrument-cbmc/identifier_names_illegal_characters/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE winbug
22
test.c
33

44
^EXIT=0$

regression/goto-cl/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:goto-cc>" -X goto-link
2+
"$<TARGET_FILE:goto-cc>" -X goto-link -X winbug
33
)

regression/goto-cl/Fo/Fo-no-directory.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE winbug
22

33
--verbosity 10 /c main1.c main2.c /Fodir
44
^EXIT=64$

0 commit comments

Comments
 (0)