# General build options
# >> 3-valued: AUTO ON OFF, allows to detect if set by user
# this is only necessary for options set for build types!
-cvc4_option(ENABLE_ASSERTIONS " Enable assertions")
+cvc4_option(ENABLE_ASSERTIONS "Enable assertions")
cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
cvc4_option(ENABLE_DUMPING "Enable dumpin")
-cvc4_option(ENABLE_MUZZLE "completely silence CVC4; remove ALL non-result output from build")
+cvc4_option(ENABLE_MUZZLE "Enable silencing CVC4; supress ALL non-result output")
cvc4_option(ENABLE_OPTIMIZED "Enable optimization")
cvc4_option(ENABLE_PROOFS "Enable proof support")
cvc4_option(ENABLE_REPLAY "Enable the replay feature")
cvc4_option(ENABLE_STATISTICS "Enable statistics")
cvc4_option(ENABLE_VALGRIND "Enable valgrind instrumentation")
# >> 2-valued: ON OFF, for options where we don't need to detect if set by user
+option(ENABLE_COVERAGE "Enable support for gcov coverage testing" OFF)
+option(ENABLE_PROFILING "Enable support for gprof profiling" OFF)
+option(ENABLE_SHARED "Build as shared library" OFF)
# Optional dependencies
option(USE_CADICAL "Use CaDiCaL SAT solver")
set(OPT_LEVEL 3)
set(GPL_LIBS "")
-set(BUILD_TYPES production debug testing competition)
+set(BUILD_TYPES Production Debug Testing Competition)
#-----------------------------------------------------------------------------#
# CVC4 build variables
endif()
message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
-if(CMAKE_BUILD_TYPE STREQUAL "debug")
+if(CMAKE_BUILD_TYPE STREQUAL "Debug")
include(ConfigDebug)
-elseif(CMAKE_BUILD_TYPE STREQUAL "production")
+elseif(CMAKE_BUILD_TYPE STREQUAL "Production")
include(ConfigProduction)
-elseif(CMAKE_BUILD_TYPE STREQUAL "testing")
+elseif(CMAKE_BUILD_TYPE STREQUAL "Testing")
include(ConfigTesting)
-elseif(CMAKE_BUILD_TYPE STREQUAL "competition")
+elseif(CMAKE_BUILD_TYPE STREQUAL "Competition")
include(ConfigCompetition)
# enable_static=yes
#TODO
add_definitions(-DCVC4_ASSERTIONS)
endif()
+if(ENABLE_COVERAGE)
+ include(CodeCoverage)
+ APPEND_COVERAGE_COMPILER_FLAGS()
+ add_definitions(-DCVC4_COVERAGE)
+ # TODO set_up_target_for_coverage + regression tests
+endif()
+
if(ENABLE_DUMPING)
add_definitions(-DCVC4_DUMPING)
else()
add_definitions(-DCVC4_MUZZLE)
endif()
+if(ENABLE_PROFILING)
+ add_definitions(-DCVC4_PROFILING)
+ add_check_c_cxx_flag("-pg")
+endif()
+
if(ENABLE_PROOFS)
#TODO RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--enable-proof"
add_definitions(-DCVC4_PROOF)
set(CVC4_TRACING 1)
endif()
+if(ENABLE_SHARED)
+ set(BUILD_SHARED_LIBS ON)
+endif()
+
if(ENABLE_STATISTICS)
add_definitions(-DCVC4_STATISTICS_ON)
endif()
message("Tracing : ${ENABLE_TRACING}")
message("Dumping : ${ENABLE_DUMPING}")
message("Muzzle : ${ENABLE_MUZZLE}")
-#message("")
+message("")
#message("Unit tests : ${support_unit_tests}")
-#message("gcov support : ${enable_coverage}")
-#message("gprof support: ${enable_profiling}")
+message("gcov support : ${ENABLE_COVERAGE}")
+message("gprof support : ${ENABLE_PROFILING}")
#message("")
#message("Static libs : ${enable_static}")
#message("Shared libs : ${enable_shared}")
--- /dev/null
+# Copyright (c) 2012 - 2017, Lars Bilke
+# All rights reserved.
+#
+# Redistribution and use in source and binary forms, with or without modification,
+# are permitted provided that the following conditions are met:
+#
+# 1. Redistributions of source code must retain the above copyright notice, this
+# list of conditions and the following disclaimer.
+#
+# 2. Redistributions in binary form must reproduce the above copyright notice,
+# this list of conditions and the following disclaimer in the documentation
+# and/or other materials provided with the distribution.
+#
+# 3. Neither the name of the copyright holder nor the names of its contributors
+# may be used to endorse or promote products derived from this software without
+# specific prior written permission.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+# ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+# WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+# DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+# ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+# (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+# ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+# (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# CHANGES:
+#
+# 2012-01-31, Lars Bilke
+# - Enable Code Coverage
+#
+# 2013-09-17, Joakim Söderberg
+# - Added support for Clang.
+# - Some additional usage instructions.
+#
+# 2016-02-03, Lars Bilke
+# - Refactored functions to use named parameters
+#
+# 2017-06-02, Lars Bilke
+# - Merged with modified version from github.com/ufz/ogs
+#
+#
+# USAGE:
+#
+# 1. Copy this file into your cmake modules path.
+#
+# 2. Add the following line to your CMakeLists.txt:
+# include(CodeCoverage)
+#
+# 3. Append necessary compiler flags:
+# APPEND_COVERAGE_COMPILER_FLAGS()
+#
+# 4. If you need to exclude additional directories from the report, specify them
+# using the COVERAGE_LCOV_EXCLUDES variable before calling SETUP_TARGET_FOR_COVERAGE_LCOV.
+# Example:
+# set(COVERAGE_LCOV_EXCLUDES 'dir1/*' 'dir2/*')
+#
+# 5. Use the functions described below to create a custom make target which
+# runs your test executable and produces a code coverage report.
+#
+# 6. Build a Debug build:
+# cmake -DCMAKE_BUILD_TYPE=Debug ..
+# make
+# make my_coverage_target
+#
+
+include(CMakeParseArguments)
+
+# Check prereqs
+find_program( GCOV_PATH gcov )
+find_program( LCOV_PATH NAMES lcov lcov.bat lcov.exe lcov.perl)
+find_program( GENHTML_PATH NAMES genhtml genhtml.perl genhtml.bat )
+find_program( GCOVR_PATH gcovr PATHS ${CMAKE_SOURCE_DIR}/scripts/test)
+find_program( SIMPLE_PYTHON_EXECUTABLE python )
+
+if(NOT GCOV_PATH)
+ message(FATAL_ERROR "gcov not found! Aborting...")
+endif() # NOT GCOV_PATH
+
+if("${CMAKE_CXX_COMPILER_ID}" MATCHES "(Apple)?[Cc]lang")
+ if("${CMAKE_CXX_COMPILER_VERSION}" VERSION_LESS 3)
+ message(FATAL_ERROR "Clang version must be 3.0.0 or greater! Aborting...")
+ endif()
+elseif(NOT CMAKE_COMPILER_IS_GNUCXX)
+ message(FATAL_ERROR "Compiler is not GNU gcc! Aborting...")
+endif()
+
+set(COVERAGE_COMPILER_FLAGS "-g -O0 --coverage -fprofile-arcs -ftest-coverage"
+ CACHE INTERNAL "")
+
+set(CMAKE_CXX_FLAGS_COVERAGE
+ ${COVERAGE_COMPILER_FLAGS}
+ CACHE STRING "Flags used by the C++ compiler during coverage builds."
+ FORCE )
+set(CMAKE_C_FLAGS_COVERAGE
+ ${COVERAGE_COMPILER_FLAGS}
+ CACHE STRING "Flags used by the C compiler during coverage builds."
+ FORCE )
+set(CMAKE_EXE_LINKER_FLAGS_COVERAGE
+ ""
+ CACHE STRING "Flags used for linking binaries during coverage builds."
+ FORCE )
+set(CMAKE_SHARED_LINKER_FLAGS_COVERAGE
+ ""
+ CACHE STRING "Flags used by the shared libraries linker during coverage builds."
+ FORCE )
+mark_as_advanced(
+ CMAKE_CXX_FLAGS_COVERAGE
+ CMAKE_C_FLAGS_COVERAGE
+ CMAKE_EXE_LINKER_FLAGS_COVERAGE
+ CMAKE_SHARED_LINKER_FLAGS_COVERAGE )
+
+if(NOT CMAKE_BUILD_TYPE STREQUAL "Debug")
+ message(WARNING "Code coverage results with an optimised (non-Debug) build may be misleading")
+endif() # NOT CMAKE_BUILD_TYPE STREQUAL "Debug"
+
+if(CMAKE_C_COMPILER_ID STREQUAL "GNU")
+ link_libraries(gcov)
+else()
+ set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} --coverage")
+endif()
+
+# Defines a target for running and collection code coverage information
+# Builds dependencies, runs the given executable and outputs reports.
+# NOTE! The executable should always have a ZERO as exit code otherwise
+# the coverage generation will not complete.
+#
+# SETUP_TARGET_FOR_COVERAGE_LCOV(
+# NAME testrunner_coverage # New target name
+# EXECUTABLE testrunner -j ${PROCESSOR_COUNT} # Executable in PROJECT_BINARY_DIR
+# DEPENDENCIES testrunner # Dependencies to build first
+# )
+function(SETUP_TARGET_FOR_COVERAGE_LCOV)
+
+ set(options NONE)
+ set(oneValueArgs NAME)
+ set(multiValueArgs EXECUTABLE EXECUTABLE_ARGS DEPENDENCIES)
+ cmake_parse_arguments(Coverage "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})
+
+ if(NOT LCOV_PATH)
+ message(FATAL_ERROR "lcov not found! Aborting...")
+ endif() # NOT LCOV_PATH
+
+ if(NOT GENHTML_PATH)
+ message(FATAL_ERROR "genhtml not found! Aborting...")
+ endif() # NOT GENHTML_PATH
+
+ # Setup target
+ add_custom_target(${Coverage_NAME}
+
+ # Cleanup lcov
+ COMMAND ${LCOV_PATH} --directory . --zerocounters
+ # Create baseline to make sure untouched files show up in the report
+ COMMAND ${LCOV_PATH} -c -i -d . -o ${Coverage_NAME}.base
+
+ # Run tests
+ COMMAND ${Coverage_EXECUTABLE}
+
+ # Capturing lcov counters and generating report
+ COMMAND ${LCOV_PATH} --directory . --capture --output-file ${Coverage_NAME}.info
+ # add baseline counters
+ COMMAND ${LCOV_PATH} -a ${Coverage_NAME}.base -a ${Coverage_NAME}.info --output-file ${Coverage_NAME}.total
+ COMMAND ${LCOV_PATH} --remove ${Coverage_NAME}.total ${COVERAGE_LCOV_EXCLUDES} --output-file ${PROJECT_BINARY_DIR}/${Coverage_NAME}.info.cleaned
+ COMMAND ${GENHTML_PATH} -o ${Coverage_NAME} ${PROJECT_BINARY_DIR}/${Coverage_NAME}.info.cleaned
+ COMMAND ${CMAKE_COMMAND} -E remove ${Coverage_NAME}.base ${Coverage_NAME}.total ${PROJECT_BINARY_DIR}/${Coverage_NAME}.info.cleaned
+
+ WORKING_DIRECTORY ${PROJECT_BINARY_DIR}
+ DEPENDS ${Coverage_DEPENDENCIES}
+ COMMENT "Resetting code coverage counters to zero.\nProcessing code coverage counters and generating report."
+ )
+
+ # Show where to find the lcov info report
+ add_custom_command(TARGET ${Coverage_NAME} POST_BUILD
+ COMMAND ;
+ COMMENT "Lcov code coverage info report saved in ${Coverage_NAME}.info."
+ )
+
+ # Show info where to find the report
+ add_custom_command(TARGET ${Coverage_NAME} POST_BUILD
+ COMMAND ;
+ COMMENT "Open ./${Coverage_NAME}/index.html in your browser to view the coverage report."
+ )
+
+endfunction() # SETUP_TARGET_FOR_COVERAGE_LCOV
+
+# Defines a target for running and collection code coverage information
+# Builds dependencies, runs the given executable and outputs reports.
+# NOTE! The executable should always have a ZERO as exit code otherwise
+# the coverage generation will not complete.
+#
+# SETUP_TARGET_FOR_COVERAGE_GCOVR_XML(
+# NAME ctest_coverage # New target name
+# EXECUTABLE ctest -j ${PROCESSOR_COUNT} # Executable in PROJECT_BINARY_DIR
+# DEPENDENCIES executable_target # Dependencies to build first
+# )
+function(SETUP_TARGET_FOR_COVERAGE_GCOVR_XML)
+
+ set(options NONE)
+ set(oneValueArgs NAME)
+ set(multiValueArgs EXECUTABLE EXECUTABLE_ARGS DEPENDENCIES)
+ cmake_parse_arguments(Coverage "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})
+
+ if(NOT SIMPLE_PYTHON_EXECUTABLE)
+ message(FATAL_ERROR "python not found! Aborting...")
+ endif() # NOT SIMPLE_PYTHON_EXECUTABLE
+
+ if(NOT GCOVR_PATH)
+ message(FATAL_ERROR "gcovr not found! Aborting...")
+ endif() # NOT GCOVR_PATH
+
+ # Combine excludes to several -e arguments
+ set(GCOVR_EXCLUDES "")
+ foreach(EXCLUDE ${COVERAGE_GCOVR_EXCLUDES})
+ list(APPEND GCOVR_EXCLUDES "-e")
+ list(APPEND GCOVR_EXCLUDES "${EXCLUDE}")
+ endforeach()
+
+ add_custom_target(${Coverage_NAME}
+ # Run tests
+ ${Coverage_EXECUTABLE}
+
+ # Running gcovr
+ COMMAND ${GCOVR_PATH} --xml
+ -r ${PROJECT_SOURCE_DIR} ${GCOVR_EXCLUDES}
+ --object-directory=${PROJECT_BINARY_DIR}
+ -o ${Coverage_NAME}.xml
+ WORKING_DIRECTORY ${PROJECT_BINARY_DIR}
+ DEPENDS ${Coverage_DEPENDENCIES}
+ COMMENT "Running gcovr to produce Cobertura code coverage report."
+ )
+
+ # Show info where to find the report
+ add_custom_command(TARGET ${Coverage_NAME} POST_BUILD
+ COMMAND ;
+ COMMENT "Cobertura code coverage report saved in ${Coverage_NAME}.xml."
+ )
+
+endfunction() # SETUP_TARGET_FOR_COVERAGE_GCOVR_XML
+
+# Defines a target for running and collection code coverage information
+# Builds dependencies, runs the given executable and outputs reports.
+# NOTE! The executable should always have a ZERO as exit code otherwise
+# the coverage generation will not complete.
+#
+# SETUP_TARGET_FOR_COVERAGE_GCOVR_HTML(
+# NAME ctest_coverage # New target name
+# EXECUTABLE ctest -j ${PROCESSOR_COUNT} # Executable in PROJECT_BINARY_DIR
+# DEPENDENCIES executable_target # Dependencies to build first
+# )
+function(SETUP_TARGET_FOR_COVERAGE_GCOVR_HTML)
+
+ set(options NONE)
+ set(oneValueArgs NAME)
+ set(multiValueArgs EXECUTABLE EXECUTABLE_ARGS DEPENDENCIES)
+ cmake_parse_arguments(Coverage "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})
+
+ if(NOT SIMPLE_PYTHON_EXECUTABLE)
+ message(FATAL_ERROR "python not found! Aborting...")
+ endif() # NOT SIMPLE_PYTHON_EXECUTABLE
+
+ if(NOT GCOVR_PATH)
+ message(FATAL_ERROR "gcovr not found! Aborting...")
+ endif() # NOT GCOVR_PATH
+
+ # Combine excludes to several -e arguments
+ set(GCOVR_EXCLUDES "")
+ foreach(EXCLUDE ${COVERAGE_GCOVR_EXCLUDES})
+ list(APPEND GCOVR_EXCLUDES "-e")
+ list(APPEND GCOVR_EXCLUDES "${EXCLUDE}")
+ endforeach()
+
+ add_custom_target(${Coverage_NAME}
+ # Run tests
+ ${Coverage_EXECUTABLE}
+
+ # Create folder
+ COMMAND ${CMAKE_COMMAND} -E make_directory ${PROJECT_BINARY_DIR}/${Coverage_NAME}
+
+ # Running gcovr
+ COMMAND ${GCOVR_PATH} --html --html-details
+ -r ${PROJECT_SOURCE_DIR} ${GCOVR_EXCLUDES}
+ --object-directory=${PROJECT_BINARY_DIR}
+ -o ${Coverage_NAME}/index.html
+ WORKING_DIRECTORY ${PROJECT_BINARY_DIR}
+ DEPENDS ${Coverage_DEPENDENCIES}
+ COMMENT "Running gcovr to produce HTML code coverage report."
+ )
+
+ # Show info where to find the report
+ add_custom_command(TARGET ${Coverage_NAME} POST_BUILD
+ COMMAND ;
+ COMMENT "Open ./${Coverage_NAME}/index.html in your browser to view the coverage report."
+ )
+
+endfunction() # SETUP_TARGET_FOR_COVERAGE_GCOVR_HTML
+
+function(APPEND_COVERAGE_COMPILER_FLAGS)
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${COVERAGE_COMPILER_FLAGS}" PARENT_SCOPE)
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${COVERAGE_COMPILER_FLAGS}" PARENT_SCOPE)
+ message(STATUS "Appending code coverage compiler flags: ${COVERAGE_COMPILER_FLAGS}")
+endfunction() # APPEND_COVERAGE_COMPILER_FLAGS
projects / cvc5.git / commitdiff