Build coverage reports using CMake

Understanding which code is covered by our tests may in future enable automation
to check whether code modifications are covered by tests.

Author: tautschnig

CMakeLists.txt

@@ -39,6 +39,44 @@ if(${enable_cbmc_tests})
     enable_testing()
 endif()
 
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
+   "${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang" OR
+   "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
+)
+    set(enable_coverage off CACHE BOOL "Build with coverage recording")
+    set(parallel_tests "1" CACHE STRING "Number of tests to run in parallel")
+    if(${enable_coverage})
+        set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} --coverage -g")
+        set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} --coverage -g")
+        if (NOT DEFINED CODE_COVERAGE_OUTPUT_DIR)
+            set(CODE_COVERAGE_OUTPUT_DIR ${CMAKE_BINARY_DIR}/html)
+            set(CODE_COVERAGE_INFO_FILE ${CODE_COVERAGE_OUTPUT_DIR}/coverage.info)
+        endif()
+        find_program(CODE_COVERAGE_LCOV lcov)
+        find_program(CODE_COVERAGE_GENHTML genhtml)
+        add_custom_target(coverage
+            COMMAND ${CMAKE_COMMAND} -E make_directory ${CODE_COVERAGE_OUTPUT_DIR}
+            COMMAND ctest -V -L CORE -j${parallel_tests}
+            COMMAND ${CODE_COVERAGE_LCOV} ${LCOV_FLAGS} --capture --directory ${CMAKE_BINARY_DIR} --output-file ${CODE_COVERAGE_INFO_FILE}
+            COMMAND ${CODE_COVERAGE_LCOV} ${LCOV_FLAGS} --remove ${CODE_COVERAGE_INFO_FILE} '/usr/*' --output-file ${CODE_COVERAGE_INFO_FILE}
+            COMMAND ${CODE_COVERAGE_GENHTML} ${CODE_COVERAGE_INFO_FILE} --output-directory ${CODE_COVERAGE_OUTPUT_DIR}
+            DEPENDS
+              java-models-library java-unit unit
+              "$<TARGET_FILE:cbmc>"
+              "$<TARGET_FILE:driver>"
+              "$<TARGET_FILE:goto-analyzer>"
+              "$<TARGET_FILE:goto-cc>"
+              "$<TARGET_FILE:goto-diff>"
+              "$<TARGET_FILE:goto-instrument>"
+              "$<TARGET_FILE:janalyzer>"
+              "$<TARGET_FILE:jbmc>"
+              "$<TARGET_FILE:jdiff>"
+              "$<TARGET_FILE:smt2_solver>"
+            WORKING_DIRECTORY ${CMAKE_BINARY_DIR}
+        )
+    endif()
+endif()
+
 add_subdirectory(src)
 add_subdirectory(regression)
 add_subdirectory(unit)

doc/architectural/compilation-and-development.md

@@ -179,6 +179,23 @@ For more information on the structure of `unit/` and how to tag tests, see
 repository](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#unit-tests)
 
 
+\subsection compilation-and-development-subsection-coverage Test coverage
+
+On Unix-style systems you can automatically generate a code coverage report. To
+obtain an HTML report for the test and unit tests, first build the dedicated
+coverage configuration using CMake (setting `enable_coverage` and building the
+`coverage` target):
+
+    cmake -H. -Bcov-build -Denable_coverage=1 -Dparallel_tests=2
+    make -C cov-build coverage
+
+This configures a build environment in the `cov-build/` folder with coverage
+recording at runtime enabled. The actual build (using `make` in the above case)
+will run the test suite, running `parallel_tests`-many tests concurrently (in
+the above case: 2). The HTML report is generated using `lcov` and stored in
+`cov-build/html/`.
+
+
 \subsection compilation-and-development-subsection-sat-solver Using a different SAT solver
 
 By default, CBMC will assume MiniSat 2 as the SAT back-end. Several other