Skip to content

Commit a00d0e4

Browse files
committed
Actually run goto-cc-multi-file regression suite
We had this folder in place for a while, but it was neither included in the Makefile nor the CMake-based regression test execution.
1 parent 52688d7 commit a00d0e4

File tree

3 files changed

+11
-0
lines changed

3 files changed

+11
-0
lines changed

Diff for: regression/CMakeLists.txt

+1
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,7 @@ add_subdirectory(k-induction)
7777
add_subdirectory(goto-harness)
7878
add_subdirectory(goto-harness-multi-file-project)
7979
add_subdirectory(goto-cc-file-local)
80+
add_subdirectory(goto-cc-multi-file)
8081
add_subdirectory(goto-cc-regression-gh-issue-5380)
8182
add_subdirectory(linking-goto-binaries)
8283
add_subdirectory(symtab2gb)

Diff for: regression/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@ DIRS = cbmc-shadow-memory \
5050
goto-harness \
5151
goto-harness-multi-file-project \
5252
goto-cc-file-local \
53+
goto-cc-multi-file \
5354
goto-cc-regression-gh-issue-5380 \
5455
linking-goto-binaries \
5556
symtab2gb \

Diff for: regression/goto-cc-multi-file/CMakeLists.txt

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
if(WIN32)
2+
set(is_windows true)
3+
else()
4+
set(is_windows false)
5+
endif()
6+
7+
add_test_pl_tests(
8+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}"
9+
)

0 commit comments

Comments
 (0)