diff options
| -rw-r--r-- | examples/CMakeLists.txt | 11 | ||||
| -rw-r--r-- | test/unit/CMakeLists.txt | 55 | ||||
| -rw-r--r-- | test/unit/base/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/unit/context/CMakeLists.txt | 14 | ||||
| -rw-r--r-- | test/unit/expr/CMakeLists.txt | 30 | ||||
| -rw-r--r-- | test/unit/main/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/unit/parser/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | test/unit/prop/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/unit/theory/CMakeLists.txt | 22 | ||||
| -rw-r--r-- | test/unit/util/CMakeLists.txt | 34 |
10 files changed, 102 insertions, 74 deletions
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 920727e86..a37cb9276 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -36,7 +36,7 @@ add_custom_target(runexamples # as arguments to the test executable. macro(cvc4_add_example name src_files libs output_dir) # The build target is created without the path prefix (not supported), - # e.g., for '<subdirs>/myexample.cpp' + # e.g., for '<output_dir>/myexample.cpp' # we create build target 'myexample' # and build it with 'make myexample'. # As a consequence, all build target names must be globally unique. @@ -50,15 +50,14 @@ macro(cvc4_add_example name src_files libs output_dir) target_link_libraries(${name} ${libs}) add_dependencies(examples ${name}) # The test target is prefixed with test identifier 'example/' and the path, - # e.g., for '<subdirs>/myexample.cpp' - # we create test target 'example/<subdirs>/myexample' - # and run it with 'ctest -R "example/<subdirs>/<example>"'. + # e.g., for '<output_dir>/myexample.cpp' + # we create test target 'example/<output_dir>/myexample' + # and run it with 'ctest -R "example/<output_dir>/myunittest"'. + set(example_bin_dir ${EXAMPLES_BIN_DIR}/${output_dir}) if("${output_dir}" STREQUAL "") set(example_test example/${name}) - set(example_bin_dir ${EXAMPLES_BIN_DIR}) else() set(example_test example/${output_dir}/${name}) - set(example_bin_dir ${EXAMPLES_BIN_DIR}/${output_dir}) endif() set_target_properties(${name} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${example_bin_dir}) diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 5e45654a9..3e90fb333 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -15,15 +15,29 @@ set(CVC4_CXXTEST_FLAGS_BLACK -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS) set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK}) -macro(cvc4_add_unit_test is_white name) - # cxxtest_add_test generates the unit test executables into directory - # CMAKE_BINARY_DIR/test/unit by default and does not allow to change this - # location (it's possible to set corresponding target properties with - # set_target_properties, but then the test environment does not find them). - # Hence, these are the only executables that are not generated into our - # default directory for executables (CMAKE_BINARY_DIR/bin). - cxxtest_add_test(${name} ${name}.cpp ${CMAKE_CURRENT_LIST_DIR}/${name}.h) - set_tests_properties(${name} PROPERTIES LABELS "unit") +# Generate and add unit test. +# Note: we do not use cxxtest_add_test from the FindCxxTest module since it +# does not allow test names containing '/'. +macro(cvc4_add_unit_test is_white name output_dir) + # generate the test sources + set(test_src ${CMAKE_CURRENT_BINARY_DIR}/${name}.cpp) + set(test_header ${CMAKE_CURRENT_LIST_DIR}/${name}.h) + add_custom_command( + OUTPUT ${test_src} + DEPENDS ${test_header} + COMMAND + ${CXXTEST_TESTGEN_INTERPRETER} + ${CXXTEST_TESTGEN_EXECUTABLE} + ${CXXTEST_TESTGEN_ARGS} -o ${test_src} ${test_header} + ) + set_source_files_properties(${test_src} PROPERTIES GENERATED true) + # The build target is created without the path prefix (not supported), + # e.g., for '<output_dir>/myunittest.h' + # we generate '${CMAKE_BINAR_DIR}/test/unit/<output_dir>/myunittest.cpp', + # create build target 'myunittest' + # and build it with 'make myunittest'. + # As a consequence, all build target names must be globally unique. + add_executable(${name} ${test_src} ${test_header}) target_link_libraries(${name} main-test) target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK}) if(${is_white}) @@ -33,16 +47,31 @@ macro(cvc4_add_unit_test is_white name) # code that does not properly add the override keyword to runTest(). target_compile_options(${name} PRIVATE -Wno-suggest-override) add_dependencies(units ${name}) + # Generate into bin/test/unit/<output_dir>. + set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir}) + set_target_properties(${name} + PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) + # The test target is prefixed with test identifier 'unit/' and the path, + # e.g., for '<output_dir>/myunittest.h' + # we create test target 'unit/<output_dir>/myunittest' + # and run it with 'ctest -R "example/<output_dir>/myunittest"'. + if("${output_dir}" STREQUAL "") + set(test_name unit/${name}) + else() + set(test_name unit/${output_dir}/${name}) + endif() + add_test(${test_name} ${test_bin_dir}/${name}) + set_tests_properties(${test_name} PROPERTIES LABELS "unit") if(ENABLE_COVERAGE) add_dependencies(coverage ${name}) endif() endmacro() -macro(cvc4_add_unit_test_black name) - cvc4_add_unit_test(FALSE ${name}) +macro(cvc4_add_unit_test_black name output_dir) + cvc4_add_unit_test(FALSE ${name} ${output_dir}) endmacro() -macro(cvc4_add_unit_test_white name) - cvc4_add_unit_test(TRUE ${name}) +macro(cvc4_add_unit_test_white name output_dir) + cvc4_add_unit_test(TRUE ${name} ${output_dir}) endmacro() add_subdirectory(base) diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt index 139d6d577..0a308b7a9 100644 --- a/test/unit/base/CMakeLists.txt +++ b/test/unit/base/CMakeLists.txt @@ -1,4 +1,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(map_util_black) +cvc4_add_unit_test_black(map_util_black base) diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt index 3d556ff6d..f089ac5f3 100644 --- a/test/unit/context/CMakeLists.txt +++ b/test/unit/context/CMakeLists.txt @@ -1,10 +1,10 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(cdlist_black) -cvc4_add_unit_test_black(cdmap_black) -cvc4_add_unit_test_white(cdmap_white) -cvc4_add_unit_test_black(cdo_black) -cvc4_add_unit_test_black(context_black) -cvc4_add_unit_test_black(context_mm_black) -cvc4_add_unit_test_white(context_white) +cvc4_add_unit_test_black(cdlist_black context) +cvc4_add_unit_test_black(cdmap_black context) +cvc4_add_unit_test_white(cdmap_white context) +cvc4_add_unit_test_black(cdo_black context) +cvc4_add_unit_test_black(context_black context) +cvc4_add_unit_test_black(context_mm_black context) +cvc4_add_unit_test_white(context_white context) diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 816d3bd71..575268cae 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -1,18 +1,18 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(attribute_black) -cvc4_add_unit_test_white(attribute_white) -cvc4_add_unit_test_black(expr_manager_public) -cvc4_add_unit_test_black(expr_public) -cvc4_add_unit_test_black(kind_black) -cvc4_add_unit_test_black(kind_map_black) -cvc4_add_unit_test_black(node_black) -cvc4_add_unit_test_black(node_builder_black) -cvc4_add_unit_test_black(node_manager_black) -cvc4_add_unit_test_white(node_manager_white) -cvc4_add_unit_test_black(node_self_iterator_black) -cvc4_add_unit_test_white(node_white) -cvc4_add_unit_test_black(symbol_table_black) -cvc4_add_unit_test_black(type_cardinality_public) -cvc4_add_unit_test_white(type_node_white) +cvc4_add_unit_test_black(attribute_black expr) +cvc4_add_unit_test_white(attribute_white expr) +cvc4_add_unit_test_black(expr_manager_public expr) +cvc4_add_unit_test_black(expr_public expr) +cvc4_add_unit_test_black(kind_black expr) +cvc4_add_unit_test_black(kind_map_black expr) +cvc4_add_unit_test_black(node_black expr) +cvc4_add_unit_test_black(node_builder_black expr) +cvc4_add_unit_test_black(node_manager_black expr) +cvc4_add_unit_test_white(node_manager_white expr) +cvc4_add_unit_test_black(node_self_iterator_black expr) +cvc4_add_unit_test_white(node_white expr) +cvc4_add_unit_test_black(symbol_table_black expr) +cvc4_add_unit_test_black(type_cardinality_public expr) +cvc4_add_unit_test_white(type_node_white expr) diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt index 2b2497a4b..7dbd01bd2 100644 --- a/test/unit/main/CMakeLists.txt +++ b/test/unit/main/CMakeLists.txt @@ -1,4 +1,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(interactive_shell_black) +cvc4_add_unit_test_black(interactive_shell_black main) diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt index debe8a4ce..37204f0c3 100644 --- a/test/unit/parser/CMakeLists.txt +++ b/test/unit/parser/CMakeLists.txt @@ -1,5 +1,5 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(parser_black) -cvc4_add_unit_test_black(parser_builder_black) +cvc4_add_unit_test_black(parser_black parser) +cvc4_add_unit_test_black(parser_builder_black parser) diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt index 990422445..dbb6de01d 100644 --- a/test/unit/prop/CMakeLists.txt +++ b/test/unit/prop/CMakeLists.txt @@ -1,4 +1,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_white(cnf_stream_white) +cvc4_add_unit_test_white(cnf_stream_white prop) diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 6dc627db9..a5a67cfa2 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -1,11 +1,11 @@ -cvc4_add_unit_test_white(evaluator_white) -cvc4_add_unit_test_white(logic_info_white) -cvc4_add_unit_test_white(theory_arith_white) -cvc4_add_unit_test_black(theory_black) -cvc4_add_unit_test_white(theory_bv_white) -cvc4_add_unit_test_white(theory_engine_white) -cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white) -cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white) -cvc4_add_unit_test_white(theory_strings_rewriter_white) -cvc4_add_unit_test_white(theory_white) -cvc4_add_unit_test_white(type_enumerator_white) +cvc4_add_unit_test_white(evaluator_white theory) +cvc4_add_unit_test_white(logic_info_white theory) +cvc4_add_unit_test_white(theory_arith_white theory) +cvc4_add_unit_test_black(theory_black theory) +cvc4_add_unit_test_white(theory_bv_white theory) +cvc4_add_unit_test_white(theory_engine_white theory) +cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) +cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) +cvc4_add_unit_test_white(theory_strings_rewriter_white theory) +cvc4_add_unit_test_white(theory_white theory) +cvc4_add_unit_test_white(type_enumerator_white theory) diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 79e5e78ff..0748e1059 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -1,20 +1,20 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(array_store_all_black) -cvc4_add_unit_test_white(assert_white) -cvc4_add_unit_test_black(binary_heap_black) -cvc4_add_unit_test_black(bitvector_black) -cvc4_add_unit_test_black(boolean_simplification_black) -cvc4_add_unit_test_black(cardinality_public) -cvc4_add_unit_test_white(check_white) -cvc4_add_unit_test_black(configuration_black) -cvc4_add_unit_test_black(datatype_black) -cvc4_add_unit_test_black(exception_black) -cvc4_add_unit_test_black(integer_black) -cvc4_add_unit_test_white(integer_white) -cvc4_add_unit_test_black(listener_black) -cvc4_add_unit_test_black(output_black) -cvc4_add_unit_test_black(rational_black) -cvc4_add_unit_test_white(rational_white) -cvc4_add_unit_test_black(stats_black) +cvc4_add_unit_test_black(array_store_all_black util) +cvc4_add_unit_test_white(assert_white util) +cvc4_add_unit_test_black(binary_heap_black util) +cvc4_add_unit_test_black(bitvector_black util) +cvc4_add_unit_test_black(boolean_simplification_black util) +cvc4_add_unit_test_black(cardinality_public util) +cvc4_add_unit_test_white(check_white util) +cvc4_add_unit_test_black(configuration_black util) +cvc4_add_unit_test_black(datatype_black util) +cvc4_add_unit_test_black(exception_black util) +cvc4_add_unit_test_black(integer_black util) +cvc4_add_unit_test_white(integer_white util) +cvc4_add_unit_test_black(listener_black util) +cvc4_add_unit_test_black(output_black util) +cvc4_add_unit_test_black(rational_black util) +cvc4_add_unit_test_white(rational_white util) +cvc4_add_unit_test_black(stats_black util) |