diff options
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}) |