File tree Expand file tree Collapse file tree 2 files changed +6
-6
lines changed Expand file tree Collapse file tree 2 files changed +6
-6
lines changed Original file line number Diff line number Diff line change @@ -3,7 +3,7 @@ set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
3
3
macro (add_test_pl_profile name cmdline flag profile)
4
4
add_test (
5
5
NAME "${name} -${profile} "
6
- COMMAND ${test_pl_path} -p -c ${cmdline} ${flag}
6
+ COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} ${ARGN}
7
7
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR} "
8
8
)
9
9
set_tests_properties ("${name} -${profile} " PROPERTIES
@@ -14,10 +14,10 @@ endmacro(add_test_pl_profile)
14
14
macro (add_test_pl_tests cmdline)
15
15
get_filename_component (TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME )
16
16
message (STATUS "Adding tests in directory: ${TEST_DIR_NAME} " )
17
- add_test_pl_profile("${TEST_DIR_NAME} " ${cmdline} -C CORE)
18
- add_test_pl_profile("${TEST_DIR_NAME} " ${cmdline} -T THOROUGH)
19
- add_test_pl_profile("${TEST_DIR_NAME} " ${cmdline} -F FUTURE)
20
- add_test_pl_profile("${TEST_DIR_NAME} " ${cmdline} -K KNOWNBUG)
17
+ add_test_pl_profile("${TEST_DIR_NAME} " " ${cmdline} " -C CORE ${ARGN} )
18
+ add_test_pl_profile("${TEST_DIR_NAME} " " ${cmdline} " -T THOROUGH ${ARGN} )
19
+ add_test_pl_profile("${TEST_DIR_NAME} " " ${cmdline} " -F FUTURE ${ARGN} )
20
+ add_test_pl_profile("${TEST_DIR_NAME} " " ${cmdline} " -K KNOWNBUG ${ARGN} )
21
21
endmacro (add_test_pl_tests)
22
22
23
23
add_subdirectory (ansi-c)
Original file line number Diff line number Diff line change 1
1
add_test_pl_tests(
2
- $<TARGET_FILE:cbmc> -X smt-backend
2
+ " $<TARGET_FILE:cbmc>" -X smt-backend
3
3
)
You can’t perform that action at this time.
0 commit comments