diff options
| -rw-r--r-- | CMakeLists.txt | 12 | ||||
| -rw-r--r-- | cmake/find_metasmt.cmake | 127 |
2 files changed, 77 insertions, 62 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 0b7b2869..2f162f21 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -309,20 +309,10 @@ include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake) ################################################################################ # STP include(${CMAKE_SOURCE_DIR}/cmake/find_stp.cmake) - # Z3 include(${CMAKE_SOURCE_DIR}/cmake/find_z3.cmake) - # metaSMT -option(ENABLE_SOLVER_METASMT "Enable metaSMT solver support" OFF) -if (ENABLE_SOLVER_METASMT) - message(STATUS "metaSMT solver support enabled") - set(ENABLE_METASMT 1) - include(${CMAKE_SOURCE_DIR}/cmake/find_metasmt.cmake) -else() - message(STATUS "metaSMT solver support disabled") - set(ENABLE_METASMT 0) # For config.h -endif() +include(${CMAKE_SOURCE_DIR}/cmake/find_metasmt.cmake) if ((NOT ${ENABLE_Z3}) AND (NOT ${ENABLE_STP}) AND (NOT ${ENABLE_METASMT})) message(FATAL_ERROR "No solver was specified. At least one solver is required." diff --git a/cmake/find_metasmt.cmake b/cmake/find_metasmt.cmake index 6751b31d..39079e2b 100644 --- a/cmake/find_metasmt.cmake +++ b/cmake/find_metasmt.cmake @@ -6,58 +6,83 @@ # License. See LICENSE.TXT for details. # #===------------------------------------------------------------------------===# +find_package(metaSMT QUIET CONFIG) -find_package(metaSMT CONFIG) -if (NOT metaSMT_FOUND) - message(FATAL_ERROR "metaSMT not found. Try setting `-DmetaSMT_DIR=/path` where" - " `/path` is the directory containing `metaSMTConfig.cmake`") +# Set the default so that if the following is true: +# * METASMT was found +# * ENABLE_SOLVER_METASMT is not already set as a cache variable +# +# then the default is set to `ON`. Otherwise set the default to `OFF`. +# A consequence of this is if we fail to detect METASMT the first time +# subsequent calls to CMake will not change the default. +if (metaSMT_FOUND) + set(ENABLE_SOLVER_METASMT_DEFAULT ON) +else() + set(ENABLE_SOLVER_METASMT_DEFAULT OFF) endif() -message(STATUS "metaSMT_DIR: ${metaSMT_DIR}") -list(APPEND KLEE_COMPONENT_EXTRA_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) -set(_metasmt_flags "") -set(_metasmt_defines "") -foreach (flag ${_metaSMT_CXXFLAGS_list}) - if ("${flag}" MATCHES "^-D") - # This is a define - list(APPEND _metasmt_defines "${flag}") - else() - # Regular flag - list(APPEND _metasmt_flags "${flag}") +option(ENABLE_SOLVER_METASMT + "Enable metaSMT solver support" + ${ENABLE_SOLVER_METASMT_DEFAULT} +) + +if (ENABLE_SOLVER_METASMT) + message(STATUS "metaSMT solver support enabled") + set(ENABLE_METASMT 1) # For config.h + + if (NOT metaSMT_FOUND) + message(FATAL_ERROR "metaSMT not found. Try setting `-DmetaSMT_DIR=/path` where" + " `/path` is the directory containing `metaSMTConfig.cmake`") endif() -endforeach() - -message(STATUS "metaSMT defines: ${_metasmt_defines}") -list(APPEND KLEE_COMPONENT_CXX_DEFINES ${_metasmt_defines}) - -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) -endforeach() - -set(available_metasmt_backends "BTOR" "STP" "Z3") -set(METASMT_DEFAULT_BACKEND "STP" - CACHE - STRING - "Default metaSMT backend. Availabe options ${available_metasmt_backends}") -# Provide drop down menu options in cmake-gui -set_property(CACHE METASMT_DEFAULT_BACKEND - PROPERTY STRINGS ${available_metasmt_backends}) - -# Check METASMT_DEFAULT_BACKEND has a valid value. -list(FIND available_metasmt_backends "${METASMT_DEFAULT_BACKEND}" _meta_smt_backend_index) -if ("${_meta_smt_backend_index}" EQUAL "-1") - message(FATAL_ERROR - "Invalid metaSMT default backend (\"${METASMT_DEFAULT_BACKEND}\").\n" - "Valid values are ${available_metasmt_backends}") -endif() + message(STATUS "metaSMT_DIR: ${metaSMT_DIR}") + list(APPEND KLEE_COMPONENT_EXTRA_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) + set(_metasmt_flags "") + set(_metasmt_defines "") + foreach (flag ${_metaSMT_CXXFLAGS_list}) + if ("${flag}" MATCHES "^-D") + # This is a define + list(APPEND _metasmt_defines "${flag}") + else() + # Regular flag + list(APPEND _metasmt_flags "${flag}") + endif() + endforeach() + + message(STATUS "metaSMT defines: ${_metasmt_defines}") + list(APPEND KLEE_COMPONENT_CXX_DEFINES ${_metasmt_defines}) -# Set appropriate define -list(APPEND KLEE_COMPONENT_CXX_DEFINES - -DMETASMT_DEFAULT_BACKEND_IS_${METASMT_DEFAULT_BACKEND}) + 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) + endforeach() + + set(available_metasmt_backends "BTOR" "STP" "Z3") + set(METASMT_DEFAULT_BACKEND "STP" + CACHE + STRING + "Default metaSMT backend. Availabe options ${available_metasmt_backends}") + # Provide drop down menu options in cmake-gui + set_property(CACHE METASMT_DEFAULT_BACKEND + PROPERTY STRINGS ${available_metasmt_backends}) + + # Check METASMT_DEFAULT_BACKEND has a valid value. + list(FIND available_metasmt_backends "${METASMT_DEFAULT_BACKEND}" _meta_smt_backend_index) + if ("${_meta_smt_backend_index}" EQUAL "-1") + message(FATAL_ERROR + "Invalid metaSMT default backend (\"${METASMT_DEFAULT_BACKEND}\").\n" + "Valid values are ${available_metasmt_backends}") + endif() + + # Set appropriate define + list(APPEND KLEE_COMPONENT_CXX_DEFINES + -DMETASMT_DEFAULT_BACKEND_IS_${METASMT_DEFAULT_BACKEND}) +else() + message(STATUS "metaSMT solver support disabled") + set(ENABLE_METASMT 0) # For config.h +endif() |