diff options
| author | Martin Nowack <m.nowack@imperial.ac.uk> | 2023-02-23 21:47:53 +0000 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-03-17 22:38:16 +0000 |
| commit | 3ef5c9d0cd51babb7c4ec2d7bb76d0cb7e47a65c (patch) | |
| tree | a2cb9e4c193d674b4f49634d0f546b65ce547860 | |
| parent | 7a4a9b9b47d2fe9b90cee95d68d89faa24a118d4 (diff) | |
| download | klee-3ef5c9d0cd51babb7c4ec2d7bb76d0cb7e47a65c.tar.gz | |
[cmake] Use LLVM's CMake functionality only
LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0).
37 files changed, 189 insertions, 757 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 89054a86..cf01df24 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -11,30 +11,8 @@ # Minimum CMake version and policies ############################################################################### cmake_minimum_required(VERSION 3.9.0) -if (POLICY CMP0054) - cmake_policy(SET CMP0054 NEW) -endif() - -if (POLICY CMP0042) - # Enable `MACOSX_RPATH` by default. - cmake_policy(SET CMP0042 NEW) -endif() - -if (POLICY CMP0037) - # Disallow reserved target names - cmake_policy(SET CMP0037 NEW) -endif() - -# This overrides the default flags for the different CMAKE_BUILD_TYPEs -set(CMAKE_USER_MAKE_RULES_OVERRIDE_C - "${CMAKE_CURRENT_SOURCE_DIR}/cmake/c_flags_override.cmake") -set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX - "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_flags_override.cmake") project(KLEE CXX C) -include(CheckFunctionExists) -include(CheckLibraryExists) - ############################################################################### # Project version ############################################################################### @@ -88,9 +66,10 @@ else() endif() endif() - # Reference specific library paths used during linking for install SET(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE) +# use, i.e. don't skip the full RPATH for the build tree +set(CMAKE_SKIP_BUILD_RPATH FALSE) ################################################################################ # Add our CMake module directory to the list of module search directories @@ -103,11 +82,6 @@ list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake/modules") # directly modifying CMAKE_CXX_FLAGS so that other code can be easily built with # different flags. ################################################################################ -set(KLEE_COMPONENT_EXTRA_INCLUDE_DIRS "") -set(KLEE_COMPONENT_CXX_DEFINES "") -set(KLEE_COMPONENT_CXX_FLAGS "") -set(KLEE_SOLVER_LIBRARIES "") -set(KLEE_COMPONENT_EXTRA_LIBRARIES "") ################################################################################ @@ -116,7 +90,8 @@ set(KLEE_COMPONENT_EXTRA_LIBRARIES "") option(ENABLE_KLEE_ASSERTS "Enable KLEE assertions" ON) if (ENABLE_KLEE_ASSERTS) message(STATUS "KLEE assertions enabled") - # Assume that -DNDEBUG isn't set. + # We have to add the undefine to the flags, otherwise "-D-UDNDEBUG" will be added + list(APPEND KLEE_COMPONENT_CXX_FLAGS "-UDNDEBUG") else() message(STATUS "KLEE assertions disabled") list(APPEND KLEE_COMPONENT_CXX_DEFINES "-DNDEBUG") @@ -136,47 +111,25 @@ include(CheckIncludeFile) include(CheckIncludeFileCXX) include(CheckPrototypeDefinition) include(CMakePushCheckState) -include("${CMAKE_SOURCE_DIR}/cmake/string_to_list.cmake") -include("${CMAKE_SOURCE_DIR}/cmake/klee_component_add_cxx_flag.cmake") -include("${CMAKE_SOURCE_DIR}/cmake/add_global_flag.cmake") - +include(CheckFunctionExists) +include(CheckLibraryExists) ################################################################################ # Find LLVM ################################################################################ -include(${CMAKE_SOURCE_DIR}/cmake/find_llvm.cmake) -set(NEEDED_LLVM_VARS - LLVM_PACKAGE_VERSION - LLVM_VERSION_MAJOR - LLVM_VERSION_MINOR - LLVM_VERSION_PATCH - LLVM_DEFINITIONS - LLVM_ENABLE_ASSERTIONS - LLVM_ENABLE_EH - LLVM_ENABLE_RTTI - LLVM_INCLUDE_DIRS - LLVM_LIBRARY_DIRS - LLVM_TOOLS_BINARY_DIR - LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN - TARGET_TRIPLE +find_package(LLVM REQUIRED CONFIG HINTS "${LLVM_DIR}") +message(STATUS "LLVM directory ${LLVM_DIR}") +set(LLVMCC "${LLVM_TOOLS_BINARY_DIR}/clang" + CACHE + PATH + "Path to C bitcode compiler" + ) +set(LLVMCXX "${LLVM_TOOLS_BINARY_DIR}/clang++" + CACHE + PATH + "Path to C++ bitcode compiler" ) -foreach (vname ${NEEDED_LLVM_VARS}) - message(STATUS "${vname}: \"${${vname}}\"") - if (NOT (DEFINED "${vname}")) - message(FATAL_ERROR "${vname} was not defined") - endif() -endforeach() - -set(OPTIONAL_LLVM_VARS - LLVM_BUILD_MAIN_SRC_DIR -) -foreach (vname ${OPTIONAL_LLVM_VARS}) - if (${vname}) - message(STATUS "${vname}: \"${${vname}}\"") - endif() -endforeach() - if (LLVM_ENABLE_ASSERTIONS) # Certain LLVM debugging macros only work when LLVM was built with asserts set(ENABLE_KLEE_DEBUG 1) # for config.h @@ -199,46 +152,40 @@ elseif ((NOT LLVM_ENABLE_ASSERTIONS) AND ENABLE_KLEE_ASSERTS) ) endif() -if (LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN) - list(APPEND KLEE_COMPONENT_CXX_FLAGS "-fvisibility-inlines-hidden") -endif() - - list(APPEND KLEE_COMPONENT_CXX_DEFINES ${LLVM_DEFINITIONS}) list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${LLVM_INCLUDE_DIRS}) # Find llvm-link -set(LLVM_LINK "${LLVM_TOOLS_BINARY_DIR}/llvm-link") +set(LLVM_LINK "${LLVM_TOOLS_BINARY_DIR}/llvm-link" + CACHE + PATH + "Path to bitcode linker" + ) if (NOT EXISTS "${LLVM_LINK}") message(FATAL_ERROR "Failed to find llvm-link at \"${LLVM_LINK}\"") endif() # Find llvm-ar -set(LLVM_AR "${LLVM_TOOLS_BINARY_DIR}/llvm-ar") +set(LLVM_AR "${LLVM_TOOLS_BINARY_DIR}/llvm-ar" + CACHE + PATH + "Path to bitcode archive tool" + ) if (NOT EXISTS "${LLVM_AR}") message(FATAL_ERROR "Failed to find llvm-ar at \"${LLVM_AR}\"") endif() # Find llvm-as -set(LLVM_AS "${LLVM_TOOLS_BINARY_DIR}/llvm-as") +set(LLVM_AS "${LLVM_TOOLS_BINARY_DIR}/llvm-as" + CACHE + PATH + "Path to bitcode assembly tool" + ) if (NOT EXISTS "${LLVM_AS}") message(FATAL_ERROR "Failed to find llvm-as at \"${LLVM_AS}\"") endif() ################################################################################ -# Find bitcode compiler -################################################################################ -include("${CMAKE_SOURCE_DIR}/cmake/find_bitcode_compiler.cmake") -message(STATUS "LLVMCC: ${LLVMCC}") -if (NOT EXISTS "${LLVMCC}") - message(FATAL_ERROR "Cannot find C bitcode compiler \"${LLVMCC}\"") -endif() -message(STATUS "LLVMCXX: ${LLVMCXX}") -if (NOT EXISTS "${LLVMCXX}") - message(FATAL_ERROR "Cannot find C++ bitcode compiler \"${LLVMCXX}\"") -endif() - -################################################################################ # C++ version ################################################################################ set(CMAKE_CXX_STANDARD 14) @@ -275,7 +222,7 @@ if (NOT LLVM_ENABLE_EH) if (ENABLE_SOLVER_METASMT) message(WARNING "Not disabling exceptions because metaSMT uses them") else() - klee_component_add_cxx_flag("-fno-exceptions" REQUIRED) + list(APPEND KLEE_COMPONENT_CXX_FLAGS "-fno-exceptions") endif() endif() @@ -289,7 +236,7 @@ if (NOT LLVM_ENABLE_RTTI) "This build configuration is not supported and will likely not work." "You should recompile LLVM with RTTI enabled.") else() - klee_component_add_cxx_flag("-fno-rtti" REQUIRED) + list(APPEND KLEE_COMPONENT_CXX_FLAGS "-fno-rtti") endif() endif() @@ -325,14 +272,19 @@ OPTION(ENABLE_TCMALLOC "Enable TCMalloc support" ON) if (ENABLE_TCMALLOC) message(STATUS "TCMalloc support enabled") set(TCMALLOC_HEADER "gperftools/malloc_extension.h") - find_path(TCMALLOC_INCLUDE_DIR "${TCMALLOC_HEADER}") + find_path(TCMALLOC_INCLUDE_DIR + "${TCMALLOC_HEADER}" + HINTS "${TCMALLOC_DIR}/include" + ) cmake_push_check_state() - set(CMAKE_REQUIRED_INCLUDES "${TCMALLOC_INCLUDE_DIR}") - check_include_file_cxx("${TCMALLOC_HEADER}" HAVE_GPERFTOOLS_MALLOC_EXTENSION_H) + list(APPEND CMAKE_REQUIRED_INCLUDES ${TCMALLOC_INCLUDE_DIR}) + check_include_file_CXX("${TCMALLOC_HEADER}" HAVE_GPERFTOOLS_MALLOC_EXTENSION_H) cmake_pop_check_state() + if (${HAVE_GPERFTOOLS_MALLOC_EXTENSION_H}) find_library(TCMALLOC_LIBRARIES NAMES tcmalloc tcmalloc_minimal + HINTS "${TCMALLOC_DIR}/lib" DOC "TCMalloc libraries" ) if (NOT TCMALLOC_LIBRARIES) @@ -341,15 +293,10 @@ if (ENABLE_TCMALLOC) endif() list(APPEND KLEE_COMPONENT_EXTRA_LIBRARIES ${TCMALLOC_LIBRARIES}) list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${TCMALLOC_INCLUDE_DIR}) - if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) - # TCMalloc's documentation says its safest to pass these flags when - # building with gcc because gcc can optimize assuming its using its own - # malloc. - klee_component_add_cxx_flag(-fno-builtin-malloc REQUIRED) - klee_component_add_cxx_flag(-fno-builtin-calloc REQUIRED) - klee_component_add_cxx_flag(-fno-builtin-realloc REQUIRED) - klee_component_add_cxx_flag(-fno-builtin-free REQUIRED) - endif() + # TCMalloc's documentation says its safest to pass these flags when + # building with gcc because gcc can optimize assuming its using its own + # malloc. + list(APPEND KLEE_COMPONENT_CXX_FLAGS "-fno-builtin-malloc" "-fno-builtin-calloc" "-fno-builtin-realloc" "-fno-builtin-free") else() message(FATAL_ERROR "Can't find \"${TCMALLOC_HEADER}\"") endif() @@ -363,10 +310,8 @@ endif() # Detect SQLite3 ################################################################################ find_package(SQLite3) -if (SQLITE3_FOUND) - include_directories(${SQLITE3_INCLUDE_DIRS}) -else() - message( FATAL_ERROR "SQLite3 not found, please install" ) +if (NOT SQLITE3_FOUND) + message( FATAL_ERROR "SQLite3 not found, please install" ) endif() ################################################################################ @@ -511,8 +456,6 @@ endif() ################################################################################ set(KLEE_UCLIBC_PATH "" CACHE PATH "Path to klee-uclibc root directory") set(KLEE_UCLIBC_BCA_NAME "klee-uclibc.bca") -list(APPEND KLEE_COMPONENT_CXX_DEFINES - -DKLEE_UCLIBC_BCA_NAME=\"${KLEE_UCLIBC_BCA_NAME}\") if (NOT KLEE_UCLIBC_PATH STREQUAL "") # Find the C library bitcode archive set(KLEE_UCLIBC_C_BCA "${KLEE_UCLIBC_PATH}/lib/libc.a") @@ -621,7 +564,7 @@ message(STATUS "CMAKE_CXX_FLAGS: ${CMAKE_CXX_FLAGS}") set(IS_ASAN_BUILD 0) set(IS_UBSAN_BUILD 0) set(IS_MSAN_BUILD 0) -string(REPLACE " " ";" _flags ${CMAKE_CXX_FLAGS}) +string(REPLACE " " ";" _flags "${CMAKE_CXX_FLAGS}") foreach(arg IN ITEMS ${_flags}) if (${arg} STREQUAL -fsanitize=address) set(IS_ASAN_BUILD 1) @@ -659,10 +602,10 @@ configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/CompileTimeInfo.h.cmin ) ################################################################################ -# Global include directories +# Set KLEE-specific include files ################################################################################ -include_directories("${CMAKE_BINARY_DIR}/include") -include_directories("${CMAKE_SOURCE_DIR}/include") + +set(KLEE_INCLUDE_DIRS ${CMAKE_SOURCE_DIR}/include ${CMAKE_BINARY_DIR}/include) ################################################################################ # Set default location for targets in the build directory @@ -685,7 +628,6 @@ message(STATUS "KLEE_SOLVER_LIBRARIES: '${KLEE_SOLVER_LIBRARIES}'") ################################################################################ # KLEE components ################################################################################ -include("${CMAKE_SOURCE_DIR}/cmake/klee_add_component.cmake") add_subdirectory(lib) add_subdirectory(runtime) diff --git a/README-CMake.md b/README-CMake.md index 4ea57421..965e2b02 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -87,13 +87,7 @@ cmake -DCMAKE_BUILD_TYPE=Release /path/to/klee/src * `LIT_ARGS` (STRING) - Semi-colon separated list of lit options. -* `LLVM_CONFIG_BINARY` (STRING) - Path to `llvm-config` binary. This is - only relevant if `USE_CMAKE_FIND_PACKAGE_LLVM` is `FALSE`. This is used - to detect the LLVM version and find libraries. - -* `LLVM_DIR` (STRING) - Path to `LLVMConfig.cmake`. This is only relevant if - `USE_CMAKE_FIND_PACKAGE_LLVM` is `TRUE`. This can be used to tell CMake where - it can find LLVM outside of standard directories. +* `LLVM_DIR` (STRING) - Path to the target LLVM install directory * `metaSMT_DIR` (STRING) - Provides a hint to CMake, where the metaSMT constraint solver can be found. This should be an absolute path to a directory @@ -105,7 +99,4 @@ cmake -DCMAKE_BUILD_TYPE=Release /path/to/klee/src but also exists in its build directory. This allows KLEE to link against STP in a build directory or an installed copy. -* `USE_CMAKE_FIND_PACKAGE_LLVM` (BOOLEAN) - Use `find_package(LLVM CONFIG)` - to find LLVM (instead of using `llvm-config` with `LLVM_CONFIG_BINARY`). - * `WARNINGS_AS_ERRORS` (BOOLEAN) - Treat warnings as errors when building KLEE. diff --git a/cmake/add_global_flag.cmake b/cmake/add_global_flag.cmake deleted file mode 100644 index 893e1200..00000000 --- a/cmake/add_global_flag.cmake +++ /dev/null @@ -1,55 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# The KLEE Symbolic Virtual Machine -# -# This file is distributed under the University of Illinois Open Source -# License. See LICENSE.TXT for details. -# -#===------------------------------------------------------------------------===# -include(CheckCXXCompilerFlag) -include(CheckCCompilerFlag) -include(CMakeParseArguments) - -function(add_global_cxx_flag flag) - CMAKE_PARSE_ARGUMENTS(add_global_cxx_flag "REQUIRED" "" "" ${ARGN}) - string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}") - string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - string(REPLACE "+" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - unset(HAS_${SANITIZED_FLAG_NAME}) - CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME}_CXX) - if (add_global_cxx_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME}_CXX) - message(FATAL_ERROR "The flag \"${flag}\" is required but your C++ compiler doesn't support it") - endif() - if (HAS_${SANITIZED_FLAG_NAME}_CXX) - message(STATUS "C++ compiler supports ${flag}") - # NOTE: Have to be careful here as CMAKE_CXX_FLAGS is a string - # and not a list. - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}" PARENT_SCOPE) - else() - message(STATUS "C++ compiler does not support ${flag}") - endif() -endfunction() - -function(add_global_c_flag flag) - CMAKE_PARSE_ARGUMENTS(add_global_c_flag "REQUIRED" "" "" ${ARGN}) - string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}") - string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - string(REPLACE "+" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - unset(HAS_${SANITIZED_FLAG_NAME}) - CHECK_C_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME}_C) - if (add_global_c_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME}_C) - message(FATAL_ERROR "The flag \"${flag}\" is required but your C compiler doesn't support it") - endif() - if (HAS_${SANITIZED_FLAG_NAME}_C) - message(STATUS "C compiler supports ${flag}") - # NOTE: Have to be careful here as CMAKE_C_FLAGS is a string - # and not a list. - set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}" PARENT_SCOPE) - else() - message(STATUS "C compiler does not support ${flag}") - endif() -endfunction() diff --git a/cmake/c_flags_override.cmake b/cmake/c_flags_override.cmake deleted file mode 100644 index 1064022c..00000000 --- a/cmake/c_flags_override.cmake +++ /dev/null @@ -1,24 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# The KLEE Symbolic Virtual Machine -# -# This file is distributed under the University of Illinois Open Source -# License. See LICENSE.TXT for details. -# -#===------------------------------------------------------------------------===# -# -# This file overrides the default compiler flags for CMake's built-in -# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set -# here. The main purpose is to make sure ``-DNDEBUG`` is never set by default. -# -#===------------------------------------------------------------------------===# -if (("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU")) - # Taken from Modules/Compiler/GNU.cmake but -DNDEBUG is removed - set(CMAKE_C_FLAGS_INIT "") - set(CMAKE_C_FLAGS_DEBUG_INIT "-O0 -g") - set(CMAKE_C_FLAGS_MINSIZEREL_INIT "-Os") - set(CMAKE_C_FLAGS_RELEASE_INIT "-O3") - set(CMAKE_C_FLAGS_RELWITHDEBINFO_INIT "-O2 -g") -else() - message(FATAL_ERROR "Overrides not set for compiler ${CMAKE_C_COMPILER_ID}") -endif() diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index 9e6e67ef..b8d00a6b 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -13,67 +13,18 @@ # NOTE: All these variables should be lists of flags and NOT a single string. ############################################################################### # FIXME: -Wunused-parameter fires a lot so for now suppress it. -set(GCC_AND_CLANG_WARNINGS_CXX +add_compile_options( "-Wall" "-Wextra" - "-Wno-unused-parameter") -set(GCC_AND_CLANG_WARNINGS_C - "-Wall" - "-Wextra" - "-Wno-unused-parameter") -set(GCC_ONLY_WARNINGS_C "") -set(GCC_ONLY_WARNINGS_CXX "") -set(CLANG_ONLY_WARNINGS_C "") -set(CLANG_ONLY_WARNINGS_CXX "") - -############################################################################### -# Check which warning flags are supported and use them globally -############################################################################### -set(CXX_WARNING_FLAGS_TO_CHECK "") -set(C_WARNING_FLAGS_TO_CHECK "") - -if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") - list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_CXX}) - list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS_CXX}) -elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") - list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_CXX}) - list(APPEND CXX_WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS_CXX}) -else() - message(AUTHOR_WARNING "Unknown compiler") -endif() - -if ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU") - list(APPEND C_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_C}) - list(APPEND C_WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS_C}) -elseif ("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") - list(APPEND C_WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_C}) - list(APPEND C_WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS_C}) -else() - message(AUTHOR_WARNING "Unknown compiler") -endif() - -# Loop through flags and use the ones which the compiler supports -foreach (flag ${CXX_WARNING_FLAGS_TO_CHECK}) - # Note `add_global_cxx_flag()` is used rather than - # `klee_component_add_cxx_flag()` because warning - # flags are typically useful for building everything. - add_global_cxx_flag("${flag}") -endforeach() -foreach (flag ${C_WARNING_FLAGS_TO_CHECK}) - add_global_c_flag("${flag}") -endforeach() + "-Wno-unused-parameter" +) ############################################################################### # Warnings as errors ############################################################################### option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF) if (WARNINGS_AS_ERRORS) - if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) - add_global_cxx_flag("-Werror" REQUIRED) - add_global_c_flag("-Werror" REQUIRED) - else() - message(AUTHOR_WARNING "Unknown compiler") - endif() + add_compile_options("-Werror") message(STATUS "Treating compiler warnings as errors") else() message(STATUS "Not treating compiler warnings as errors") diff --git a/cmake/cxx_flags_override.cmake b/cmake/cxx_flags_override.cmake deleted file mode 100644 index 0e3946fe..00000000 --- a/cmake/cxx_flags_override.cmake +++ /dev/null @@ -1,25 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# The KLEE Symbolic Virtual Machine -# -# This file is distributed under the University of Illinois Open Source -# License. See LICENSE.TXT for details. -# -#===------------------------------------------------------------------------===# -# -# This file overrides the default compiler flags for CMake's built-in -# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set -# here. The main purpose is to make sure ``-DNDEBUG`` is never set by default. -# -#===------------------------------------------------------------------------===# - -if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) - # Taken from Modules/Compiler/GNU.cmake but -DNDEBUG is removed - set(CMAKE_CXX_FLAGS_INIT "") - set(CMAKE_CXX_FLAGS_DEBUG_INIT "-O0 -g") - set(CMAKE_CXX_FLAGS_MINSIZEREL_INIT "-Os") - set(CMAKE_CXX_FLAGS_RELEASE_INIT "-O3") - set(CMAKE_CXX_FLAGS_RELWITHDEBINFO_INIT "-O2 -g") -else() - message(FATAL_ERROR "Overrides not set for compiler ${CMAKE_CXX_COMPILER_ID}") -endif() diff --git a/cmake/find_bitcode_compiler.cmake b/cmake/find_bitcode_compiler.cmake deleted file mode 100644 index 615931f3..00000000 --- a/cmake/find_bitcode_compiler.cmake +++ /dev/null @@ -1,96 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# The KLEE Symbolic Virtual Machine -# -# This file is distributed under the University of Illinois Open Source -# License. See LICENSE.TXT for details. -# -#===------------------------------------------------------------------------===# -# -# This file tries to find compilers to build LLVM bitcode. -# It is implicitly dependent on `find_llvm.cmake` already being run in the -# same scope. -# -#===------------------------------------------------------------------------===# - -message(STATUS "Looking for bitcode compilers") - -find_program( - LLVMCC - NAMES "clang-${LLVM_VERSION_MAJOR}.${LLVM_VERSION_MINOR}" "clang" "llvm-gcc" - # Give the LLVM tools directory higher priority than the system directory. - HINTS "${LLVM_TOOLS_BINARY_DIR}" -) -if (LLVMCC) - message(STATUS "Found ${LLVMCC}") -else() - message(FATAL_ERROR "Failed to find C bitcode compiler") -endif() - -find_program( - LLVMCXX - NAMES "clang++-${LLVM_VERSION_MAJOR}.${LLVM_VERSION_MINOR}" "clang++" "llvm-g++" - # Give the LLVM tools directory higher priority than the system directory. - HINTS "${LLVM_TOOLS_BINARY_DIR}" -) -if (LLVMCXX) - message(STATUS "Found ${LLVMCXX}") -else() - message(FATAL_ERROR "Failed to find C++ bitcode compiler") -endif() - -# Check `llvm-dis` is available -set(LLVM_DIS_TOOL "${LLVM_TOOLS_BINARY_DIR}/llvm-dis") -if (NOT EXISTS "${LLVM_DIS_TOOL}") - message(FATAL_ERROR - "The llvm-dis tool cannot be found at \"${LLVM_DIS_TOOL}\"") -endif() - -# Test compiler -function(test_bitcode_compiler COMPILER SRC_EXT) - message(STATUS "Testing bitcode compiler ${COMPILER}") - set(SRC_FILE "${CMAKE_BINARY_DIR}/test_bitcode_compiler.${SRC_EXT}") - file(WRITE "${SRC_FILE}" "int main(int argc, char** argv) { return 0;}") - set(BC_FILE "${SRC_FILE}.bc") - execute_process( - COMMAND - "${COMPILER}" - "-c" - "-emit-llvm" - "-o" "${BC_FILE}" - "${SRC_FILE}" - RESULT_VARIABLE COMPILE_INVOKE_EXIT_CODE - ) - if ("${COMPILE_INVOKE_EXIT_CODE}" EQUAL 0) - message(STATUS "Compile success") - else() - message(FATAL_ERROR "Compilation failed") - endif() - - message(STATUS "Checking compatibility with LLVM ${LLVM_PACKAGE_VERSION}") - # Check if the LLVM version we are using is compatible - # with this compiler by invoking the `llvm-dis` tool - # on the generated bitcode. - set(LL_FILE "${SRC_FILE}.ll") - execute_process( - COMMAND - "${LLVM_DIS_TOOL}" - "-o" "${LL_FILE}" - "${BC_FILE}" - RESULT_VARIABLE LLVM_DIS_INVOKE_EXIT_CODE - ) - if ("${LLVM_DIS_INVOKE_EXIT_CODE}" EQUAL 0) - message(STATUS "\"${COMPILER}\" is compatible") - else() - message(FATAL_ERROR "\"${COMPILER}\" is not compatible with LLVM ${LLVM_PACKAGE_VERSION}") - endif() - - # Remove temporary files. It's okay to not remove these on failure - # as they will be useful for developer debugging. - file(REMOVE "${SRC_FILE}") - file(REMOVE "${BC_FILE}") - file(REMOVE "${LL_FILE}") -endfunction() - -test_bitcode_compiler("${LLVMCC}" "c") -test_bitcode_compiler("${LLVMCXX}" "cxx") diff --git a/cmake/find_llvm.cmake b/cmake/find_llvm.cmake deleted file mode 100644 index 0f80a28b..00000000 --- a/cmake/find_llvm.cmake +++ /dev/null @@ -1,246 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# The KLEE Symbolic Virtual Machine -# -# This file is distributed under the University of Illinois Open Source -# License. See LICENSE.TXT for details. -# -#===------------------------------------------------------------------------===# -# -# This file provides multiple methods to detect LLVM. -# -# * llvm-config executable. This method is portable across LLVM build systems -# (i.e. works if LLVM was built with autoconf/Makefile or with CMake). -# -# * find_package(LLVM CONFIG). This method relies on the `LLVMConfig.cmake` file -# generated by LLVM's build system. -# -#===------------------------------------------------------------------------===# - -option(USE_CMAKE_FIND_PACKAGE_LLVM "Use find_package(LLVM CONFIG) to find LLVM" OFF) - -if (USE_CMAKE_FIND_PACKAGE_LLVM) - # Use find_package() to detect LLVM in the user's environment. - # The user can force a particular copy by passing - # `-DLLVM_DIR=/path/to/LLVMConfig.cmake` to CMake. - find_package(LLVM CONFIG REQUIRED) - - list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}") - include(AddLLVM) - - # Provide function to map LLVM components to libraries. - function(klee_get_llvm_libs output_var) - llvm_map_components_to_libnames(${output_var} ${ARGN}) - set(${output_var} ${${output_var}} PARENT_SCOPE) - endfunction() - - # HACK: This information is not exported so just pretend its OFF for now. - set(LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN OFF) - - # make LLVM_DEFINITIONS into proper list - set(_new_llvm_definitions "${LLVM_DEFINITIONS}") - string(REPLACE " " ";" LLVM_DEFINITIONS "${_new_llvm_definitions}") - unset(_new_llvm_definitions) -else() - # Use the llvm-config binary to get the information needed. - # Try to detect it in the user's environment. The user can force a particular - # binary by passing `-DLLVM_CONFIG_BINARY=/path/to/llvm-config` to CMake. - find_program(LLVM_CONFIG_BINARY - NAMES llvm-config) - message(STATUS "LLVM_CONFIG_BINARY: ${LLVM_CONFIG_BINARY}") - - if (NOT LLVM_CONFIG_BINARY) - message(FATAL_ERROR - "Failed to find llvm-config.\n" - "Try passing -DLLVM_CONFIG_BINARY=/path/to/llvm-config to cmake") - endif() - - function(_run_llvm_config output_var) - set(_command "${LLVM_CONFIG_BINARY}" ${ARGN}) - execute_process(COMMAND ${_command} - RESULT_VARIABLE _exit_code - OUTPUT_VARIABLE ${output_var} - OUTPUT_STRIP_TRAILING_WHITESPACE - ERROR_STRIP_TRAILING_WHITESPACE - ) - if (NOT ("${_exit_code}" EQUAL "0")) - message(FATAL_ERROR "Failed running ${_command}") - endif() - set(${output_var} ${${output_var}} PARENT_SCOPE) - endfunction() - - # Get LLVM version - _run_llvm_config(LLVM_PACKAGE_VERSION "--version") - # Try x.y.z patern - set(_llvm_version_regex "^([0-9]+)\\.([0-9]+)\\.([0-9]+)(svn|git|-rust-dev)?$") - if ("${LLVM_PACKAGE_VERSION}" MATCHES "${_llvm_version_regex}") - string(REGEX REPLACE - "${_llvm_version_regex}" - "\\1" - LLVM_VERSION_MAJOR - "${LLVM_PACKAGE_VERSION}") - string(REGEX REPLACE - "${_llvm_version_regex}" - "\\2" - LLVM_VERSION_MINOR - "${LLVM_PACKAGE_VERSION}") - string(REGEX REPLACE - "${_llvm_version_regex}" - "\\3" - LLVM_VERSION_PATCH - "${LLVM_PACKAGE_VERSION}") - else() - # try x.y pattern - set(_llvm_version_regex "^([0-9]+)\\.([0-9]+)(svn|git)?$") - if ("${LLVM_PACKAGE_VERSION}" MATCHES "${_llvm_version_regex}") - string(REGEX REPLACE - "${_llvm_version_regex}" - "\\1" - LLVM_VERSION_MAJOR - "${LLVM_PACKAGE_VERSION}") - string(REGEX REPLACE - "${_llvm_version_regex}" - "\\2" - LLVM_VERSION_MINOR - "${LLVM_PACKAGE_VERSION}") - set(LLVM_VERSION_PATCH 0) - else() - message(FATAL_ERROR - "Failed to parse LLVM version from \"${LLVM_PACKAGE_VERSION}\"") - endif() - endif() - - set(LLVM_DEFINITIONS "") - _run_llvm_config(_llvm_cpp_flags "--cppflags") - string_to_list("${_llvm_cpp_flags}" _llvm_cpp_flags_list) - foreach (flag ${_llvm_cpp_flags_list}) - # Filter out -I flags by only looking for -D flags. - if ("${flag}" MATCHES "^-D" AND NOT ("${flag}" STREQUAL "-D_DEBUG")) - list(APPEND LLVM_DEFINITIONS "${flag}") - endif() - endforeach() - - set(LLVM_ENABLE_ASSERTIONS ON) - set(LLVM_ENABLE_EH ON) - set(LLVM_ENABLE_RTTI ON) - set(LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN OFF) - _run_llvm_config(_llvm_cxx_flags "--cxxflags") - string_to_list("${_llvm_cxx_flags}" _llvm_cxx_flags_list) - foreach (flag ${_llvm_cxx_flags_list}) - if ("${flag}" STREQUAL "-DNDEBUG") - # Note we don't rely on `llvm-config --build-mode` because - # that seems broken when LLVM is built with CMake. - set(LLVM_ENABLE_ASSERTIONS OFF) - elseif ("${flag}" STREQUAL "-fno-exceptions") - set(LLVM_ENABLE_EH OFF) - elseif ("${flag}" STREQUAL "-fno-rtti") - set(LLVM_ENABLE_RTTI OFF) - elseif ("${flag}" STREQUAL "-fvisibility-inlines-hidden") - set(LLVM_ENABLE_VISIBILITY_INLINES_HIDDEN ON) - endif() - endforeach() - - set(LLVM_INCLUDE_DIRS "") - foreach (flag ${_llvm_cpp_flags_list}) - # Filter out -D flags by only looking for -I flags. - if ("${flag}" MATCHES "^-I") - string(REGEX REPLACE "^-I(.+)$" "\\1" _include_dir "${flag}") - list(APPEND LLVM_INCLUDE_DIRS "${_include_dir}") - endif() - endforeach() - - _run_llvm_config(LLVM_LIBRARY_DIRS "--libdir") - _run_llvm_config(LLVM_TOOLS_BINARY_DIR "--bindir") - _run_llvm_config(TARGET_TRIPLE "--host-target") - - _run_llvm_config(LLVM_BUILD_MAIN_SRC_DIR "--src-root") - if (NOT EXISTS "${LLVM_BUILD_MAIN_SRC_DIR}") - set(LLVM_BUILD_MAIN_SRC_DIR "") - endif() - - # Provide function to map LLVM components to libraries. - function(klee_get_llvm_libs OUTPUT_VAR) - _run_llvm_config(_llvm_libs "--libfiles" ${ARGN}) - string_to_list("${_llvm_libs}" _llvm_libs_list) - - # Now find the system libs that are needed. - _run_llvm_config(_system_libs "--system-libs") - string_to_list("${_system_libs}" _system_libs_list) - - # Create an imported target for each LLVM library - # if it doesn't already exist. We need to do this - # so we can tell CMake that these libraries depend - # on the necessary libraries so that CMake - # can get the link order right. - set(targets_to_return "") - set(created_targets "") - foreach (llvm_lib ${_llvm_libs_list}) - get_filename_component(llvm_lib_file_name "${llvm_lib}" NAME) - - string(REGEX REPLACE "^(lib)?(LLVM[-.a-zA-Z0-9]+)\\..+$" "\\2" target_name "${llvm_lib_file_name}") - list(APPEND targets_to_return "${target_name}") - if (NOT TARGET "${target_name}") - # DEBUG: message(STATUS "Creating imported target \"${target_name}\"" " for \"${llvm_lib}\"") - list(APPEND created_targets "${target_name}") - - set(import_library_type "STATIC") - if ("${llvm_lib_file_name}" MATCHES "(so|dylib|dll)$") - set(import_library_type "SHARED") - endif() - # Create an imported target for the library - add_library("${target_name}" "${import_library_type}" IMPORTED GLOBAL) - set_property(TARGET "${target_name}" PROPERTY - IMPORTED_LOCATION "${llvm_lib}" - ) - endif() - endforeach() - - # Now state the dependencies of the created imported targets which we - # assume to be for each imported target the libraries which appear after - # the library in `{_llvm_libs_list}` and then finally the system libs. - # It is **essential** that we do this otherwise CMake will get the - # link order of the imported targets wrong. - list(LENGTH targets_to_return length_targets_to_return) - if ("${length_targets_to_return}" GREATER 0) - math(EXPR targets_to_return_last_index "${length_targets_to_return} -1") - foreach (llvm_target_lib ${created_targets}) - # DEBUG: message(STATUS "Adding deps for target ${llvm_target_lib}") - # Find position in `targets_to_return` - list(FIND targets_to_return "${llvm_target_lib}" position) - if ("${position}" EQUAL "-1") - message(FATAL_ERROR "couldn't find \"${llvm_target_lib}\" in list of targets") - endif() - if ("${position}" LESS "${targets_to_return_last_index}") - math(EXPR position_plus_one "${position} + 1") - foreach (index RANGE ${position_plus_one} ${targets_to_return_last_index}) - # Get the target for this index - list(GET targets_to_return ${index} target_for_index) - # DEBUG: message(STATUS "${llvm_target_libs} depends on ${target_for_index}") - set_property(TARGET "${llvm_target_lib}" APPEND PROPERTY - INTERFACE_LINK_LIBRARIES "${target_for_index}" - ) - endforeach() - endif() - # Now finally add the system library dependencies. These must be last. - set_property(TARGET "${target_name}" APPEND PROPERTY - INTERFACE_LINK_LIBRARIES "${_system_libs_list}" - ) - endforeach() - endif() - - set(${OUTPUT_VAR} ${targets_to_return} PARENT_SCOPE) - endfunction() -endif() - -# Filter out `-DNEBUG` from LLVM_DEFINITIONS. The caller can use -# `LLVM_ENABLE_ASSERTIONS` to decide how to set their defines. -set(_new_llvm_definitions "") -foreach (llvm_define ${LLVM_DEFINITIONS}) - if ("${llvm_define}" STREQUAL "-DNDEBUG") - # Skip - else() - list(APPEND _new_llvm_definitions "${llvm_define}") - endif() -endforeach() -set(LLVM_DEFINITIONS "${_new_llvm_definitions}") -unset(_new_llvm_definitions) diff --git a/cmake/find_metasmt.cmake b/cmake/find_metasmt.cmake index 3dc9fe50..d4a2c155 100644 --- a/cmake/find_metasmt.cmake +++ b/cmake/find_metasmt.cmake @@ -34,13 +34,12 @@ if (ENABLE_SOLVER_METASMT) " `/path` is the directory containing `metaSMTConfig.cmake`") endif() message(STATUS "metaSMT_DIR: ${metaSMT_DIR}") - list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS - "${metaSMT_INCLUDE_DIR}" ${metaSMT_INCLUDE_DIRS}) + list(APPEND KLEE_SOLVER_INCLUDE_DIRS "${metaSMT_INCLUDE_DIR}" ${metaSMT_INCLUDE_DIRS}) # FIXME: We should test linking list(APPEND KLEE_SOLVER_LIBRARIES ${metaSMT_LIBRARIES}) # Separate flags and defines from ${metaSMT_CXXFLAGS} - string_to_list("${metaSMT_CXXFLAGS}" _metaSMT_CXXFLAGS_list) + string(REPLACE " " ";" _metaSMT_CXXFLAGS_list "${metaSMT_CXXFLAGS}") set(_metasmt_flags "") set(_metasmt_defines "") foreach (flag ${_metaSMT_CXXFLAGS_list}) @@ -59,12 +58,12 @@ if (ENABLE_SOLVER_METASMT) message(STATUS "metaSMT flags: ${_metasmt_flags}") foreach (f ${_metasmt_flags}) # Test the flag and fail if it can't be used - klee_component_add_cxx_flag(${f} REQUIRED) + list(APPEND KLEE_COMPONENT_CXX_FLAGS "${f}") endforeach() # Check if metaSMT provides an useable backend if (NOT metaSMT_AVAILABLE_QF_ABV_SOLVERS) - message(FATAL_ERROR "metaSMT does not provide an useable backend.") + message(FATAL_ERROR "metaSMT does not provide an usable backend.") endif() message(STATUS "metaSMT has the following backend(s): ${metaSMT_AVAILABLE_QF_ABV_SOLVERS}.") @@ -72,7 +71,7 @@ if (ENABLE_SOLVER_METASMT) set(METASMT_DEFAULT_BACKEND "STP" CACHE STRING - "Default metaSMT backend. Availabe options ${available_metasmt_backends}") + "Default metaSMT backend. Available options ${available_metasmt_backends}") # Provide drop down menu options in cmake-gui set_property(CACHE METASMT_DEFAULT_BACKEND PROPERTY STRINGS ${available_metasmt_backends}) @@ -91,6 +90,9 @@ if (ENABLE_SOLVER_METASMT) foreach(backend ${available_metasmt_backends}) list(APPEND KLEE_COMPONENT_CXX_DEFINES -DMETASMT_HAVE_${backend}) endforeach() + + # Support newer CVC4 versions + list(APPEND KLEE_COMPONENT_CXX_DEFINES CVC4_WITHOUT_KIND_IFF) else() message(STATUS "metaSMT solver support disabled") set(ENABLE_METASMT 0) # For config.h diff --git a/cmake/find_stp.cmake b/cmake/find_stp.cmake index 7b10f1fe..2206cc88 100644 --- a/cmake/find_stp.cmake +++ b/cmake/find_stp.cmake @@ -44,7 +44,7 @@ if (ENABLE_SOLVER_STP) message(STATUS "Using STP shared library") list(APPEND KLEE_SOLVER_LIBRARIES "${STP_SHARED_LIBRARY}") endif() - list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS "${STP_INCLUDE_DIRS}") + list(APPEND KLEE_SOLVER_INCLUDE_DIRS ${STP_INCLUDE_DIRS}) message(STATUS "STP_DIR: ${STP_DIR}") set(ENABLE_STP 1) # For config.h else() diff --git a/cmake/find_z3.cmake b/cmake/find_z3.cmake index 823cc051..c4e96fd7 100644 --- a/cmake/find_z3.cmake +++ b/cmake/find_z3.cmake @@ -26,6 +26,8 @@ option(ENABLE_SOLVER_Z3 "Enable Z3 solver support" ${ENABLE_SOLVER_Z3_DEFAULT}) if (ENABLE_SOLVER_Z3) message(STATUS "Z3 solver support enabled") if (Z3_FOUND) + include(CheckCXXSourceCompiles) + message(STATUS "Found Z3") set(ENABLE_Z3 1) # For config.h list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${Z3_INCLUDE_DIRS}) @@ -51,6 +53,10 @@ if (ENABLE_SOLVER_Z3) else() message(STATUS "Z3_get_error_msg does not require context") endif() + + list(APPEND KLEE_SOLVER_INCLUDE_DIRS ${Z3_INCLUDE_DIRS}) + list(APPEND KLEE_SOLVER_LIBRARY_DIRS ${Z3_LIBRARIES}) + else() message(FATAL_ERROR "Z3 not found.") endif() diff --git a/cmake/klee_add_component.cmake b/cmake/klee_add_component.cmake deleted file mode 100644 index 4f9770ac..00000000 --- a/cmake/klee_add_component.cmake +++ /dev/null @@ -1,20 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# The KLEE Symbolic Virtual Machine -# -# This file is distributed under the University of Illinois Open Source -# License. See LICENSE.TXT for details. -# -#===------------------------------------------------------------------------===# - -function(klee_add_component target_name) - # Components are explicitly STATIC because we don't support building them - # as shared libraries. - add_library(${target_name} STATIC ${ARGN}) - # In newer CMakes we can make sure that the flags are only used when compiling C++ - target_compile_options(${target_name} PUBLIC - $<$<COMPILE_LANGUAGE:CXX>:${KLEE_COMPONENT_CXX_FLAGS}>) - target_include_directories(${target_name} PUBLIC ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS}) - target_compile_definitions(${target_name} PUBLIC ${KLEE_COMPONENT_CXX_DEFINES}) - target_link_libraries(${target_name} PUBLIC ${KLEE_COMPONENT_EXTRA_LIBRARIES}) -endfunction() diff --git a/cmake/klee_component_add_cxx_flag.cmake b/cmake/klee_component_add_cxx_flag.cmake deleted file mode 100644 index c866f6da..00000000 --- a/cmake/klee_component_add_cxx_flag.cmake +++ /dev/null @@ -1,31 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# The KLEE Symbolic Virtual Machine -# -# This file is distributed under the University of Illinois Open Source -# License. See LICENSE.TXT for details. -# -#===------------------------------------------------------------------------===# -include(CheckCXXCompilerFlag) -include(CMakeParseArguments) - -function(klee_component_add_cxx_flag flag) - CMAKE_PARSE_ARGUMENTS(klee_component_add_cxx_flag "REQUIRED" "" "" ${ARGN}) - string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}") - string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - string(REPLACE "+" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") - unset(HAS_${SANITIZED_FLAG_NAME}) - CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME}) - if (klee_component_add_cxx_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME}) - message(FATAL_ERROR "The flag \"${flag}\" is required but your C++ compiler doesn't support it") - endif() - if (HAS_${SANITIZED_FLAG_NAME}) - message(STATUS "C++ compiler supports ${flag}") - list(APPEND KLEE_COMPONENT_CXX_FLAGS "${flag}") - set(KLEE_COMPONENT_CXX_FLAGS ${KLEE_COMPONENT_CXX_FLAGS} PARENT_SCOPE) - else() - message(STATUS "C++ compiler does not support ${flag}") - endif() -endfunction() diff --git a/cmake/string_to_list.cmake b/cmake/string_to_list.cmake deleted file mode 100644 index 65c04413..00000000 --- a/cmake/string_to_list.cmake +++ /dev/null @@ -1,13 +0,0 @@ -#===------------------------------------------------------------------------===# -# -# The KLEE Symbolic Virtual Machine -# -# This file is distributed under the University of Illinois Open Source -# License. See LICENSE.TXT for details. -# -#===------------------------------------------------------------------------===# - -function(string_to_list s output_var) - string(REPLACE " " ";" _output "${s}") - set(${output_var} ${_output} PARENT_SCOPE) -endfunction() diff --git a/lib/Basic/CMakeLists.txt b/lib/Basic/CMakeLists.txt index d156116f..5671c144 100644 --- a/lib/Basic/CMakeLists.txt +++ b/lib/Basic/CMakeLists.txt @@ -6,13 +6,14 @@ # License. See LICENSE.TXT for details. # #===------------------------------------------------------------------------===# -klee_add_component(kleeBasic +add_library(kleeBasic KTest.cpp Statistics.cpp ) -set(LLVM_COMPONENTS - support -) -klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS}) -target_link_libraries(kleeBasic PUBLIC ${LLVM_LIBS}) +llvm_map_components_to_libnames(llvm_libs support) +target_link_libraries(kleeBasic PRIVATE ${llvm_libs}) +target_compile_options(kleeBasic PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(kleeBasic PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +target_include_directories(kleeBasic PRIVATE ${KLEE_INCLUDE_DIRS}) diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index de52cd11..0905a7f0 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -6,7 +6,7 @@ # License. See LICENSE.TXT for details. # #===------------------------------------------------------------------------===# -klee_add_component(kleeCore +add_library(kleeCore AddressSpace.cpp MergeHandler.cpp CallPathManager.cpp @@ -28,18 +28,6 @@ klee_add_component(kleeCore UserSearcher.cpp ) -# TODO: Work out what the correct LLVM components are for -# kleeCore. -set(LLVM_COMPONENTS - core - executionengine - mcjit - native - support -) - -klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS}) -target_link_libraries(kleeCore PUBLIC ${LLVM_LIBS} ${SQLITE3_LIBRARIES}) target_link_libraries(kleeCore PRIVATE kleeBasic kleeModule @@ -47,3 +35,9 @@ target_link_libraries(kleeCore PRIVATE kleaverExpr kleeSupport ) + +llvm_map_components_to_libnames(llvm_libs core executionengine mcjit native support) +target_link_libraries(kleeCore PRIVATE ${llvm_libs} ${SQLITE3_LIBRARIES}) +target_include_directories(kleeCore PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS} ${SQLITE3_INCLUDE_DIRS}) +target_compile_options(kleeCore PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(kleeCore PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) diff --git a/lib/Expr/CMakeLists.txt b/lib/Expr/CMakeLists.txt index f469a1de..6b8a873b 100644 --- a/lib/Expr/CMakeLists.txt +++ b/lib/Expr/CMakeLists.txt @@ -6,7 +6,7 @@ # License. See LICENSE.TXT for details. # #===------------------------------------------------------------------------===# -klee_add_component(kleaverExpr +add_library(kleaverExpr ArrayCache.cpp ArrayExprOptimizer.cpp ArrayExprRewriter.cpp @@ -26,8 +26,8 @@ klee_add_component(kleaverExpr Updates.cpp ) -set(LLVM_COMPONENTS - support -) -klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS}) -target_link_libraries(kleaverExpr PUBLIC ${LLVM_LIBS}) +llvm_map_components_to_libnames(llvm_libs support) +target_link_libraries(kleaverExpr PRIVATE ${llvm_libs}) +target_include_directories(kleaverExpr PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS}) +target_compile_options(kleaverExpr PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(kleaverExpr PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt index 6c2a24b3..c81d395e 100644 --- a/lib/Module/CMakeLists.txt +++ b/lib/Module/CMakeLists.txt @@ -22,22 +22,31 @@ set(KLEE_MODULE_COMPONENT_SRCS RaiseAsm.cpp ) -klee_add_component(kleeModule +add_library(kleeModule ${KLEE_MODULE_COMPONENT_SRCS} ) -set(LLVM_COMPONENTS - bitreader +llvm_map_components_to_libnames(llvm_libs bitreader bitwriter codegen ipo irreader linker support -) + scalaropts + instcombine + transformutils + analysis + object + mc + binaryformat + ) + +target_link_libraries(kleeModule PRIVATE ${llvm_libs}) -klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS}) -target_link_libraries(kleeModule PUBLIC ${LLVM_LIBS}) target_link_libraries(kleeModule PRIVATE kleeSupport ) +target_include_directories(kleeModule PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS}) +target_compile_options(kleeModule PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(kleeModule PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt index 31c8302a..81a64882 100644 --- a/lib/Solver/CMakeLists.txt +++ b/lib/Solver/CMakeLists.txt @@ -6,7 +6,7 @@ # License. See LICENSE.TXT for details. # #===------------------------------------------------------------------------===# -klee_add_component(kleaverSolver +add_library(kleaverSolver AssignmentValidatingSolver.cpp CachingSolver.cpp CexCachingSolver.cpp @@ -32,15 +32,14 @@ klee_add_component(kleaverSolver Z3Solver.cpp ) -set(LLVM_COMPONENTS - support -) -klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS}) -target_link_libraries(kleaverSolver PUBLIC ${LLVM_LIBS}) - +llvm_map_components_to_libnames(llvm_libs support) target_link_libraries(kleaverSolver PRIVATE kleeBasic kleaverExpr kleeSupport - ${KLEE_SOLVER_LIBRARIES}) + ${KLEE_SOLVER_LIBRARIES} ${llvm_libs}) +target_include_directories(kleaverSolver PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS} ${KLEE_SOLVER_INCLUDE_DIRS}) +target_compile_options(kleaverSolver PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(kleaverSolver PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + diff --git a/lib/Support/CMakeLists.txt b/lib/Support/CMakeLists.txt index 7145930f..7ff4daa3 100644 --- a/lib/Support/CMakeLists.txt +++ b/lib/Support/CMakeLists.txt @@ -6,7 +6,7 @@ # License. See LICENSE.TXT for details. # #===------------------------------------------------------------------------===# -klee_add_component(kleeSupport +add_library(kleeSupport CompressionStream.cpp ErrorHandling.cpp FileHandling.cpp @@ -18,10 +18,9 @@ klee_add_component(kleeSupport TreeStream.cpp ) -target_link_libraries(kleeSupport PRIVATE ${ZLIB_LIBRARIES}) +llvm_map_components_to_libnames(llvm_libs support) -set(LLVM_COMPONENTS - support -) -klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS}) -target_link_libraries(kleeSupport PUBLIC ${LLVM_LIBS}) +target_link_libraries(kleeSupport PRIVATE ${llvm_libs} ${ZLIB_LIBRARIES} ${TCMALLOC_LIBRARIES}) +target_include_directories(kleeSupport PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS} ${TCMALLOC_INCLUDE_DIR}) +target_compile_options(kleeSupport PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(kleeSupport PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) diff --git a/runtime/Runtest/CMakeLists.txt b/runtime/Runtest/CMakeLists.txt index 9ae185ee..df5f2c23 100644 --- a/runtime/Runtest/CMakeLists.txt +++ b/runtime/Runtest/CMakeLists.txt @@ -20,6 +20,6 @@ set_target_properties(kleeRuntest VERSION ${KLEE_RUNTEST_VERSION} SOVERSION ${KLEE_RUNTEST_VERSION} ) +target_include_directories(kleeRuntest PRIVATE ${KLEE_INCLUDE_DIRS}) -install(TARGETS kleeRuntest - DESTINATION "${CMAKE_INSTALL_FULL_LIBDIR}") +install(TARGETS kleeRuntest DESTINATION "${CMAKE_INSTALL_FULL_LIBDIR}") diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 6a625935..226eb08a 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -96,10 +96,8 @@ if (DOWNLOAD_FILECHECK_SOURCE) add_executable(FileCheck ${FILECHECK_SRC_FILE} ) - klee_get_llvm_libs(FILECHECK_NEEDED_LIBS Support) - target_include_directories(FileCheck PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS}) - target_compile_options(FileCheck PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) - target_compile_definitions(FileCheck PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + llvm_map_components_to_libnames(FILECHECK_NEEDED_LIBS support) + target_include_directories(FileCheck PRIVATE ${LLVM_INCLUDE_DIRS}) target_link_libraries(FileCheck PRIVATE ${FILECHECK_NEEDED_LIBS}) endif() @@ -119,10 +117,8 @@ if (DOWNLOAD_NOT_SOURCE) add_executable("not" ${NOT_SRC_FILE} ) - klee_get_llvm_libs(NOT_NEEDED_LIBS Support) - target_include_directories("not" PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS}) - target_compile_options("not" PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) - target_compile_definitions("not" PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + llvm_map_components_to_libnames(NOT_NEEDED_LIBS support) + target_include_directories("not" PRIVATE ${LLVM_INCLUDE_DIRS}) target_link_libraries("not" PRIVATE ${NOT_NEEDED_LIBS}) endif() diff --git a/tools/kleaver/CMakeLists.txt b/tools/kleaver/CMakeLists.txt index c079c2a4..acc681e5 100644 --- a/tools/kleaver/CMakeLists.txt +++ b/tools/kleaver/CMakeLists.txt @@ -10,10 +10,14 @@ add_executable(kleaver main.cpp ) -set(KLEE_LIBS - kleaverSolver -) +llvm_map_components_to_libnames(llvm_libs core support) + +target_link_libraries(kleaver kleaverSolver ${llvm_libs}) +target_include_directories(kleaver PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS}) +target_compile_options(kleaver PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(kleaver PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +target_compile_definitions(kleaver PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) -target_link_libraries(kleaver ${KLEE_LIBS}) install(TARGETS kleaver RUNTIME DESTINATION bin) diff --git a/tools/klee-replay/CMakeLists.txt b/tools/klee-replay/CMakeLists.txt index aeb90845..83fddaeb 100644 --- a/tools/klee-replay/CMakeLists.txt +++ b/tools/klee-replay/CMakeLists.txt @@ -15,6 +15,7 @@ if (HAVE_PTY_H OR HAVE_UTIL_H OR HAVE_LIBUTIL_H) ) target_link_libraries(klee-replay PRIVATE kleeBasic) + target_include_directories(klee-replay PRIVATE ${KLEE_INCLUDE_DIRS}) if(LIBCAP_LIBRARIES) target_link_libraries(klee-replay PRIVATE ${LIBCAP_LIBRARIES}) diff --git a/tools/klee/CMakeLists.txt b/tools/klee/CMakeLists.txt index 8b05c357..cabdfdfc 100644 --- a/tools/klee/CMakeLists.txt +++ b/tools/klee/CMakeLists.txt @@ -15,6 +15,10 @@ set(KLEE_LIBS ) target_link_libraries(klee ${KLEE_LIBS}) +target_include_directories(klee PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS}) +target_compile_options(klee PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(klee PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + install(TARGETS klee RUNTIME DESTINATION bin) diff --git a/tools/ktest-gen/CMakeLists.txt b/tools/ktest-gen/CMakeLists.txt index 084d551d..2bd9af6b 100644 --- a/tools/ktest-gen/CMakeLists.txt +++ b/tools/ktest-gen/CMakeLists.txt @@ -13,5 +13,6 @@ add_executable(ktest-gen set(KLEE_LIBS kleeBasic) target_link_libraries(ktest-gen ${KLEE_LIBS}) +target_include_directories(ktest-gen PRIVATE ${KLEE_INCLUDE_DIRS}) install(TARGETS ktest-gen RUNTIME DESTINATION bin) diff --git a/tools/ktest-randgen/CMakeLists.txt b/tools/ktest-randgen/CMakeLists.txt index 8b15c275..48b23485 100644 --- a/tools/ktest-randgen/CMakeLists.txt +++ b/tools/ktest-randgen/CMakeLists.txt @@ -13,5 +13,6 @@ add_executable(ktest-randgen set(KLEE_LIBS kleeBasic) target_link_libraries(ktest-randgen ${KLEE_LIBS}) +target_include_directories(ktest-randgen PRIVATE ${KLEE_INCLUDE_DIRS}) install(TARGETS ktest-randgen RUNTIME DESTINATION bin) diff --git a/unittests/Assignment/CMakeLists.txt b/unittests/Assignment/CMakeLists.txt index e5dd1b4c..647aae4c 100644 --- a/unittests/Assignment/CMakeLists.txt +++ b/unittests/Assignment/CMakeLists.txt @@ -1,3 +1,7 @@ add_klee_unit_test(AssignmentTest AssignmentTest.cpp) target_link_libraries(AssignmentTest PRIVATE kleaverExpr kleaverSolver) +target_compile_options(AssignmentTest PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(AssignmentTest PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +target_include_directories(AssignmentTest PRIVATE ${KLEE_INCLUDE_DIRS}) diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt index 88d5de91..9e30a9b7 100644 --- a/unittests/CMakeLists.txt +++ b/unittests/CMakeLists.txt @@ -46,9 +46,9 @@ endfunction() if (TARGET gtest) # try to reuse LLVM's 'gtest' target - message(WARNING "LLVM exports its 'gtest' CMake target (for Google Test), so" - "KLEE cannot create its own. Thus, KLEE will reuse the existing one. This" - "is, however, only recommended if LLVM and KLEE were built using the same" + message(WARNING "LLVM exports its 'gtest' CMake target (for Google Test), so " + "KLEE cannot create its own. Thus, KLEE will reuse the existing one. This " + "is, however, only recommended if LLVM and KLEE were built using the same " "compiler and linker flags (to prevent compatibility issues).\n" "To prevent CMake from reusing the target or to use a different version " "of Google Test, try either of the following:\n" @@ -166,6 +166,8 @@ else() endif() endif() +enable_testing() + # This keeps track of all the unit test # targets so we can ensure they are built @@ -199,7 +201,8 @@ endif() add_library(unittest_main) target_sources(unittest_main PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/TestMain.cpp") -klee_get_llvm_libs(UNITTEST_MAIN_LIBS Support) +llvm_map_components_to_libnames(UNITTEST_MAIN_LIBS support) + target_link_libraries(unittest_main PUBLIC ${GTEST_TARGET_NAME} diff --git a/unittests/DiscretePDF/CMakeLists.txt b/unittests/DiscretePDF/CMakeLists.txt index 07ec1f89..f3b23fc9 100644 --- a/unittests/DiscretePDF/CMakeLists.txt +++ b/unittests/DiscretePDF/CMakeLists.txt @@ -1,4 +1,8 @@ add_klee_unit_test(DiscretePDFTest DiscretePDFTest.cpp) # FIXME add the following line to link against libgtest.a -target_link_libraries(DiscretePDFTest PRIVATE kleaverSolver) \ No newline at end of file +target_link_libraries(DiscretePDFTest PRIVATE kleaverSolver) +target_compile_options(DiscretePDFTest PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(DiscretePDFTest PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +target_include_directories(DiscretePDFTest PRIVATE ${KLEE_INCLUDE_DIRS}) diff --git a/unittests/Expr/CMakeLists.txt b/unittests/Expr/CMakeLists.txt index 34bc5a01..56646715 100644 --- a/unittests/Expr/CMakeLists.txt +++ b/unittests/Expr/CMakeLists.txt @@ -2,3 +2,8 @@ add_klee_unit_test(ExprTest ExprTest.cpp ArrayExprTest.cpp) target_link_libraries(ExprTest PRIVATE kleaverExpr kleeSupport kleaverSolver) +target_compile_options(ExprTest PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(ExprTest PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +target_include_directories(ExprTest PRIVATE ${KLEE_INCLUDE_DIRS}) + diff --git a/unittests/RNG/CMakeLists.txt b/unittests/RNG/CMakeLists.txt index 866f9158..67363323 100644 --- a/unittests/RNG/CMakeLists.txt +++ b/unittests/RNG/CMakeLists.txt @@ -1,3 +1,7 @@ add_klee_unit_test(RNGTest RNGTest.cpp) target_link_libraries(RNGTest PRIVATE kleeSupport) +target_compile_options(RNGTest PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(RNGTest PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +target_include_directories(RNGTest PRIVATE ${KLEE_INCLUDE_DIRS}) diff --git a/unittests/Ref/CMakeLists.txt b/unittests/Ref/CMakeLists.txt index facd26a3..f60927d8 100644 --- a/unittests/Ref/CMakeLists.txt +++ b/unittests/Ref/CMakeLists.txt @@ -1,3 +1,7 @@ add_klee_unit_test(RefTest RefTest.cpp) target_link_libraries(RefTest PRIVATE kleaverExpr) +target_compile_options(RefTest PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(RefTest PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +target_include_directories(RefTest PRIVATE ${KLEE_INCLUDE_DIRS}) diff --git a/unittests/Searcher/CMakeLists.txt b/unittests/Searcher/CMakeLists.txt index 29358470..c35b407f 100644 --- a/unittests/Searcher/CMakeLists.txt +++ b/unittests/Searcher/CMakeLists.txt @@ -1,4 +1,8 @@ add_klee_unit_test(SearcherTest SearcherTest.cpp) target_link_libraries(SearcherTest PRIVATE kleeCore) -target_include_directories(SearcherTest BEFORE PUBLIC "../../lib") +target_include_directories(SearcherTest BEFORE PRIVATE "${CMAKE_SOURCE_DIR}/lib") +target_compile_options(SearcherTest PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(SearcherTest PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +target_include_directories(SearcherTest PRIVATE ${KLEE_INCLUDE_DIRS}) \ No newline at end of file diff --git a/unittests/Solver/CMakeLists.txt b/unittests/Solver/CMakeLists.txt index c3dc63b6..c3cd357c 100644 --- a/unittests/Solver/CMakeLists.txt +++ b/unittests/Solver/CMakeLists.txt @@ -1,9 +1,16 @@ add_klee_unit_test(SolverTest SolverTest.cpp) target_link_libraries(SolverTest PRIVATE kleaverSolver) +target_compile_options(SolverTest PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(SolverTest PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) +target_include_directories(SolverTest PRIVATE ${KLEE_INCLUDE_DIRS}) + if (${ENABLE_Z3}) add_klee_unit_test(Z3SolverTest Z3SolverTest.cpp) -target_link_libraries(Z3SolverTest PRIVATE kleaverSolver) + target_link_libraries(Z3SolverTest PRIVATE kleaverSolver) + target_compile_options(Z3SolverTest PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) + target_compile_definitions(Z3SolverTest PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + target_include_directories(Z3SolverTest PRIVATE ${KLEE_INCLUDE_DIRS}) endif() diff --git a/unittests/Time/CMakeLists.txt b/unittests/Time/CMakeLists.txt index 6a860582..0280a4bb 100644 --- a/unittests/Time/CMakeLists.txt +++ b/unittests/Time/CMakeLists.txt @@ -1,3 +1,6 @@ add_klee_unit_test(TimeTest TimeTest.cpp) target_link_libraries(TimeTest PRIVATE kleeSupport) +target_compile_options(TimeTest PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(TimeTest PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) +target_include_directories(TimeTest PRIVATE ${KLEE_INCLUDE_DIRS}) diff --git a/unittests/TreeStream/CMakeLists.txt b/unittests/TreeStream/CMakeLists.txt index ff9b4c3e..db9ef3db 100644 --- a/unittests/TreeStream/CMakeLists.txt +++ b/unittests/TreeStream/CMakeLists.txt @@ -1,3 +1,6 @@ add_klee_unit_test(TreeStreamTest TreeStreamTest.cpp) target_link_libraries(TreeStreamTest PRIVATE kleeBasic kleeSupport) +target_compile_options(TreeStreamTest PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(TreeStreamTest PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) +target_include_directories(TreeStreamTest PRIVATE ${KLEE_INCLUDE_DIRS}) |