2017-08-31 00:10:45 +08:00
|
|
|
cmake_minimum_required(VERSION 3.2)
|
|
|
|
|
2017-09-01 22:36:36 +08:00
|
|
|
find_program(CCACHE_PROGRAM ccache)
|
|
|
|
if(CCACHE_PROGRAM)
|
|
|
|
set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
|
2017-09-14 05:03:57 +08:00
|
|
|
message(STATUS "Rule launch compile: ${CCACHE_PROGRAM}")
|
2017-09-01 22:36:36 +08:00
|
|
|
endif()
|
|
|
|
|
2017-09-18 05:08:59 +08:00
|
|
|
set(CMAKE_EXPORT_COMPILE_COMMANDS true)
|
|
|
|
|
2017-08-31 00:17:38 +08:00
|
|
|
set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
|
|
|
|
|
2017-08-31 00:10:45 +08:00
|
|
|
include(GNUInstallDirs)
|
|
|
|
|
2017-08-31 00:17:38 +08:00
|
|
|
set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
|
|
|
|
set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
|
|
|
|
set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
|
2017-08-31 00:10:45 +08:00
|
|
|
|
2017-09-08 18:16:26 +08:00
|
|
|
if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
|
2018-06-22 22:09:57 +08:00
|
|
|
"${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang" OR
|
2017-09-08 18:16:26 +08:00
|
|
|
"${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
|
|
|
|
)
|
|
|
|
# Ensure NDEBUG is not set for release builds
|
|
|
|
set(CMAKE_CXX_FLAGS_RELEASE "-O2")
|
2019-01-26 00:29:40 +08:00
|
|
|
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g")
|
2017-09-08 18:16:26 +08:00
|
|
|
# Enable lots of warnings
|
2018-04-12 00:31:39 +08:00
|
|
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations")
|
2017-09-08 18:16:26 +08:00
|
|
|
elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
|
|
|
|
# This would be the place to enable warnings for Windows builds, although
|
|
|
|
# config.inc doesn't seem to do that currently
|
|
|
|
endif()
|
|
|
|
|
2017-08-31 00:17:38 +08:00
|
|
|
set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
|
|
|
|
|
2017-09-08 17:05:51 +08:00
|
|
|
set(sat_impl "minisat2" CACHE STRING
|
|
|
|
"This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
|
|
|
|
)
|
|
|
|
|
2017-08-31 00:17:38 +08:00
|
|
|
if(${enable_cbmc_tests})
|
|
|
|
enable_testing()
|
|
|
|
endif()
|
2018-05-23 19:04:45 +08:00
|
|
|
|
2019-01-15 20:56:15 +08:00
|
|
|
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()
|
|
|
|
|
2018-05-23 19:04:45 +08:00
|
|
|
add_subdirectory(src)
|
2017-08-31 00:17:38 +08:00
|
|
|
add_subdirectory(regression)
|
2018-05-23 19:04:45 +08:00
|
|
|
add_subdirectory(unit)
|
|
|
|
|
|
|
|
add_subdirectory(jbmc)
|
2017-11-15 23:55:08 +08:00
|
|
|
|
|
|
|
set_target_properties(
|
|
|
|
analyses
|
|
|
|
ansi-c
|
|
|
|
assembler
|
|
|
|
big-int
|
|
|
|
cbmc
|
|
|
|
cbmc-lib
|
|
|
|
cpp
|
|
|
|
driver
|
|
|
|
goto-analyzer
|
|
|
|
goto-analyzer-lib
|
|
|
|
goto-cc
|
|
|
|
goto-cc-lib
|
2018-12-15 20:07:07 +08:00
|
|
|
goto-checker
|
2017-11-15 23:55:08 +08:00
|
|
|
goto-diff
|
|
|
|
goto-diff-lib
|
2019-01-22 00:16:34 +08:00
|
|
|
goto-harness
|
2017-11-15 23:55:08 +08:00
|
|
|
goto-instrument
|
|
|
|
goto-instrument-lib
|
|
|
|
goto-programs
|
|
|
|
goto-symex
|
|
|
|
jsil
|
|
|
|
json
|
2017-02-24 02:39:14 +08:00
|
|
|
json-symtab-language
|
2017-11-15 23:55:08 +08:00
|
|
|
langapi
|
|
|
|
linking
|
|
|
|
pointer-analysis
|
|
|
|
solvers
|
|
|
|
testing-utils
|
|
|
|
unit
|
|
|
|
util
|
|
|
|
xml
|
|
|
|
|
2018-05-16 16:59:49 +08:00
|
|
|
java_bytecode
|
2018-06-24 01:45:27 +08:00
|
|
|
java-models-library
|
2018-05-16 16:59:49 +08:00
|
|
|
jbmc
|
|
|
|
jbmc-lib
|
2018-05-18 17:47:38 +08:00
|
|
|
janalyzer
|
|
|
|
janalyzer-lib
|
2018-05-18 17:46:49 +08:00
|
|
|
jdiff
|
|
|
|
jdiff-lib
|
2018-05-16 16:59:49 +08:00
|
|
|
java-testing-utils
|
|
|
|
java-unit
|
|
|
|
miniz
|
|
|
|
|
2017-11-15 23:55:08 +08:00
|
|
|
PROPERTIES
|
|
|
|
CXX_STANDARD 11
|
|
|
|
CXX_STANDARD_REQUIRED true
|
|
|
|
XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
|
|
|
|
)
|