Skip to content

Commit c2ab3ff

Browse files
committed
Move regression test into dedicated API regression folder
1 parent ada16d5 commit c2ab3ff

File tree

7 files changed

+29
-2
lines changed

7 files changed

+29
-2
lines changed

.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,7 @@ regression/**/*.smt2
6565
regression/solver-hardness/solver-hardness-simple/solver_hardness.json
6666
jbmc/regression/**/tests.log
6767
jbmc/regression/**/tests-symex-driven-loading.log
68+
cprover-cpp-api/regression/**/tests.log
6869

6970
# regression/coverage file
7071
/regression/coverage_**

CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ option(WITH_MEMORY_ANALYZER
206206
add_subdirectory(src)
207207
add_subdirectory(regression)
208208
add_subdirectory(unit)
209-
add_subdirectory(cpp_api)
209+
add_subdirectory(cprover-cpp-api)
210210

211211
cprover_default_properties(
212212
analyses

cprover-cpp-api/regression/CMakeLists.txt

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,30 @@ target_include_directories(api-binary-driver
1010
${CMAKE_CURRENT_SOURCE_DIR}/../src)
1111
target_link_libraries(api-binary-driver goto-programs util langapi ansi-c)
1212

13+
# Enable test running
14+
set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl")
15+
16+
macro(add_test_pl_profile name cmdline flag profile)
17+
add_test(
18+
NAME "${name}-${profile}"
19+
COMMAND perl ${test_pl_path} -e -p -c "${cmdline}" ${flag} ${ARGN}
20+
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
21+
)
22+
set_tests_properties("${name}-${profile}" PROPERTIES
23+
LABELS "${profile};CBMC"
24+
)
25+
endmacro(add_test_pl_profile)
26+
27+
macro(add_test_pl_tests cmdline)
28+
get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
29+
message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}")
30+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE ${ARGN})
31+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN})
32+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN})
33+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
34+
endmacro(add_test_pl_tests)
35+
36+
# For the best possible utilisation of multiple cores when
37+
# running tests in parallel, it is important that these directories are
38+
# listed with decreasing runtimes (i.e. longest running at the top)
39+
add_subdirectory(model_loading)

regression/CMakeLists.txt

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,6 @@ add_subdirectory(cbmc-concurrency)
3737
add_subdirectory(cbmc-cover)
3838
add_subdirectory(cbmc-incr-oneloop)
3939
add_subdirectory(cbmc-incr-smt2)
40-
add_subdirectory(cprover-api-cpp)
4140
add_subdirectory(cbmc-incr)
4241
add_subdirectory(cbmc-output-file)
4342
add_subdirectory(cbmc-with-incr)

0 commit comments

Comments
 (0)