From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 22 Aug 2018 15:46:50 +0000 (-0700)
Subject: cmake: Add dependencies for test targets and support for make coverage.
X-Git-Tag: cvc5-1.0.0~4586
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=38c24575b3415f375b14ebfb7685a1621c7587e2;p=cvc5.git

cmake: Add dependencies for test targets and support for make coverage.
---

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 36c372652..74f223e22 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -255,7 +255,10 @@ if(ENABLE_COVERAGE)
   include(CodeCoverage)
   APPEND_COVERAGE_COMPILER_FLAGS()
   add_definitions(-DCVC4_COVERAGE)
-  # TODO set_up_target_for_coverage + regression tests
+  setup_target_for_coverage_lcov(
+    NAME coverage
+    EXECUTABLE ctest $(ARGS)
+    DEPENDENCIES cvc4-bin)
 endif()
 
 if(ENABLE_DUMPING)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0d29ad52c..32194dbee 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1998,6 +1998,10 @@ set(regression_disabled_tests
 get_target_property(path_to_cvc4 cvc4-bin RUNTIME_OUTPUT_DIRECTORY)
 set(run_regress_script ${CMAKE_CURRENT_LIST_DIR}/run_regression.py)
 
+add_custom_target(regress
+  COMMAND ctest --output-on-failure -L "regress[0-1]" $(ARGS)
+  DEPENDS cvc4-bin)
+
 macro(cvc4_add_regression_test level file)
   add_test(${file}
     ${run_regress_script}
@@ -2025,5 +2029,3 @@ endforeach()
 foreach(file ${regress_4_tests})
   cvc4_add_regression_test(4 ${file})
 endforeach()
-
-add_custom_target(regress COMMAND ctest --output-on-failure -L "regress[0-1]" $(ARGS))
diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt
index 694cad171..0ae2806d4 100644
--- a/test/system/CMakeLists.txt
+++ b/test/system/CMakeLists.txt
@@ -3,6 +3,8 @@ include_directories(${PROJECT_SOURCE_DIR}/src)
 include_directories(${PROJECT_SOURCE_DIR}/src/include)
 include_directories(${CMAKE_BINARY_DIR}/src)
 
+add_custom_target(systemtests COMMAND ctest --output-on-failure -L "system" $(ARGS))
+
 set(CVC4_SYSTEM_TEST_FLAGS
   -D__BUILDING_CVC4_SYSTEM_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
 
@@ -13,6 +15,10 @@ macro(cvc4_add_system_test name)
   target_compile_definitions(${name} PRIVATE ${CVC4_SYSTEM_TEST_FLAGS})
   add_test(system/${name} ${CMAKE_CURRENT_BINARY_DIR}/${name})
   set_tests_properties(system/${name} PROPERTIES LABELS "system")
+  add_dependencies(systemtests ${name})
+  if(ENABLE_COVERAGE)
+    add_dependencies(coverage ${name})
+  endif()
 endmacro()
 
 cvc4_add_system_test(boilerplate)
@@ -23,5 +29,3 @@ cvc4_add_system_test(smt2_compliance)
 cvc4_add_system_test(statistics)
 cvc4_add_system_test(two_smt_engines)
 #TODO java test (needs bindings)
-
-add_custom_target(systemtests COMMAND ctest --output-on-failure -L "system" $(ARGS))
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 088dc7cc7..f91c5b35e 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -1,42 +1,44 @@
-if(ENABLE_UNIT_TESTING)
-  include_directories(.)
-  include_directories(${PROJECT_SOURCE_DIR}/src)
-  include_directories(${PROJECT_SOURCE_DIR}/src/include)
-  include_directories(${CMAKE_BINARY_DIR}/src)
+include_directories(.)
+include_directories(${PROJECT_SOURCE_DIR}/src)
+include_directories(${PROJECT_SOURCE_DIR}/src/include)
+include_directories(${CMAKE_BINARY_DIR}/src)
 
-  set(CVC4_CXXTEST_FLAGS_BLACK
-    -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
-    -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
-  set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK})
+add_custom_target(units COMMAND ctest -L "unit" $(ARGS))
 
-  macro(cvc4_add_unit_test is_white name)
-    cxxtest_add_test(${name} ${name}.cpp ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
-    set_tests_properties(${name} PROPERTIES LABELS "unit")
-    target_link_libraries(${name} main)
-    target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK})
-    if(${is_white})
-      target_compile_options(${name} PRIVATE -fno-access-control)
-    endif()
-    # Disable the Wsuggest-override warnings for the unit tests. CxxTest generates
-    # code that does not properly add the override keyword to runTest().
-    target_compile_options(${name} PRIVATE -Wno-suggest-override)
-  endmacro()
+set(CVC4_CXXTEST_FLAGS_BLACK
+  -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
+  -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_black name)
-    cvc4_add_unit_test(FALSE ${name})
-  endmacro()
-  macro(cvc4_add_unit_test_white name)
-    cvc4_add_unit_test(TRUE ${name})
-  endmacro()
+macro(cvc4_add_unit_test is_white name)
+  cxxtest_add_test(${name} ${name}.cpp ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
+  set_tests_properties(${name} PROPERTIES LABELS "unit")
+  target_link_libraries(${name} main)
+  target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK})
+  if(${is_white})
+    target_compile_options(${name} PRIVATE -fno-access-control)
+  endif()
+  # Disable the Wsuggest-override warnings for the unit tests. CxxTest generates
+  # code that does not properly add the override keyword to runTest().
+  target_compile_options(${name} PRIVATE -Wno-suggest-override)
+  add_dependencies(units ${name})
+  if(ENABLE_COVERAGE)
+    add_dependencies(coverage ${name})
+  endif()
+endmacro()
 
-  add_subdirectory(base)
-  add_subdirectory(context)
-  add_subdirectory(expr)
-  add_subdirectory(main)
-  add_subdirectory(parser)
-  add_subdirectory(prop)
-  add_subdirectory(theory)
-  add_subdirectory(util)
+macro(cvc4_add_unit_test_black name)
+  cvc4_add_unit_test(FALSE ${name})
+endmacro()
+macro(cvc4_add_unit_test_white name)
+  cvc4_add_unit_test(TRUE ${name})
+endmacro()
 
-  add_custom_target(units COMMAND ctest -L "unit" $(ARGS))
-endif()
+add_subdirectory(base)
+add_subdirectory(context)
+add_subdirectory(expr)
+add_subdirectory(main)
+add_subdirectory(parser)
+add_subdirectory(prop)
+add_subdirectory(theory)
+add_subdirectory(util)