about summary refs log tree commit diff homepage
path: root/cmake
diff options
context:
space:
mode:
Diffstat (limited to 'cmake')
-rw-r--r--cmake/add_global_flag.cmake55
-rw-r--r--cmake/c_flags_override.cmake24
-rw-r--r--cmake/compiler_warnings.cmake57
-rw-r--r--cmake/cxx_flags_override.cmake25
-rw-r--r--cmake/find_bitcode_compiler.cmake96
-rw-r--r--cmake/find_llvm.cmake246
-rw-r--r--cmake/find_metasmt.cmake14
-rw-r--r--cmake/find_stp.cmake2
-rw-r--r--cmake/find_z3.cmake6
-rw-r--r--cmake/klee_add_component.cmake20
-rw-r--r--cmake/klee_component_add_cxx_flag.cmake31
-rw-r--r--cmake/string_to_list.cmake13
12 files changed, 19 insertions, 570 deletions
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()
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-23 11:05:21 +0000