about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.common9
-rw-r--r--Makefile.config.in1
-rw-r--r--autoconf/configure.ac90
-rwxr-xr-xconfigure78
-rw-r--r--include/klee/CommandLine.h4
-rw-r--r--include/klee/Config/config.h.in12
-rw-r--r--include/klee/Solver.h6
-rw-r--r--lib/Basic/CmdLineOptions.cpp27
-rw-r--r--lib/Solver/CoreSolver.cpp11
-rw-r--r--lib/Solver/MetaSMTBuilder.h4
-rw-r--r--lib/Solver/MetaSMTSolver.cpp6
-rw-r--r--lib/Solver/STPBuilder.cpp5
-rw-r--r--lib/Solver/STPSolver.cpp4
-rw-r--r--tools/kleaver/Makefile4
-rw-r--r--tools/kleaver/main.cpp4
-rw-r--r--tools/klee/Makefile4
-rw-r--r--unittests/Expr/Makefile1
-rw-r--r--unittests/Ref/Makefile2
-rw-r--r--unittests/Solver/Makefile4
19 files changed, 169 insertions, 107 deletions
diff --git a/Makefile.common b/Makefile.common
index 7b210118..4ec1d4c6 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -61,7 +61,11 @@ endif
 # This is filename that KLEE will look for when trying to load klee-uclibc
 KLEE_UCLIBC_BCA_NAME="klee-uclibc.bca"
 
-CXX.Flags += $(STP_CFLAGS)
+ifneq ($(ENABLE_STP),0)
+  CXX.Flags += $(STP_CFLAGS)
+  CXX.Flags += -DEXT_HASH_MAP
+endif
+
 CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_INSTALL_BIN_DIR=\"$(PROJ_bindir)\"
 CXX.Flags += -DKLEE_INSTALL_RUNTIME_DIR=\"$(BYTECODE_DESTINATION)\"
 
@@ -69,9 +73,6 @@ ifeq ($(ENABLE_UCLIBC),1)
 	CXX.Flags += -DKLEE_UCLIBC_BCA_NAME=\"$(KLEE_UCLIBC_BCA_NAME)\"
 endif
 
-# For STP.
-CXX.Flags += -DEXT_HASH_MAP
-
 # For metaSMT
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
diff --git a/Makefile.config.in b/Makefile.config.in
index 5b9f929c..745b4cc1 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -29,6 +29,7 @@ PROJ_INSTALL_ROOT := @prefix@
 
 KLEE_USE_CXX11 := @KLEE_USE_CXX11@
 
+ENABLE_STP := @ENABLE_STP@
 STP_CFLAGS := @STP_CFLAGS@
 STP_LDFLAGS := @STP_LDFLAGS@
 
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 3d4becc8..8ba6a029 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -553,58 +553,70 @@ dnl **************************************************************************
 dnl Find an install of STP
 dnl **************************************************************************
 
+ENABLE_STP=0
 AC_ARG_WITH(stp,
   AS_HELP_STRING([--with-stp],
     [Location of STP installation directory]),[
       #Check for empty argument
       if test "X$withval" = X ; then
-	      AC_MSG_ERROR([<path> cannot be empty in --with-stp=<path>])
+        AC_MSG_ERROR([<path> cannot be empty in --with-stp=<path>])
       fi
       stp_root=`(cd $withval && pwd) 2> /dev/null`
 
       #Check for bad path
       if test "X$stp_root" = X ; then
-	    AC_MSG_ERROR([Cannot access path $with_stp passed to --with-stp])
+        AC_MSG_ERROR([Cannot access path $with_stp passed to --with-stp])
       fi
 
       STP_CFLAGS="-I$stp_root/include"
       STP_LDFLAGS="-L$stp_root/lib"
+      ENABLE_STP=1
     ])
 
-old_CPPFLAGS="$CPPFLAGS"
-CPPFLAGS="$CPPFLAGS $STP_CFLAGS"
-AC_CHECK_HEADER(stp/c_interface.h,,
-    [
-        AC_MSG_ERROR([Unable to use stp/c_interface.h header])
-    ])
-CPPFLAGS="$old_CPPFLAGS"
-
-STP_NEEDS_MINISAT=0
-AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [
-       STP_NEEDS_MINISAT=1; AC_MSG_RESULT([Could not link with libstp])
-], "$STP_LDFLAGS")
-
-dnl Try linking again with minisat if necessary
-if test "X$STP_NEEDS_MINISAT" != X0 ; then
-  # Need to clear cached result
-  unset ac_cv_lib_stp_vc_setInterfaceFlags
-
-  AC_CHECK_LIB(stp,
-	       vc_setInterfaceFlags,, [
-	       AC_MSG_ERROR([Unable to link with libstp. Check config.log to see what went wrong])
-  ], "$STP_LDFLAGS" "-lminisat" )
-
-  STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat"
+if test "X$ENABLE_STP" != X0; then
+    old_CPPFLAGS="$CPPFLAGS"
+    CPPFLAGS="$CPPFLAGS $STP_CFLAGS"
+    AC_CHECK_HEADER(stp/c_interface.h,,
+        [
+            AC_MSG_ERROR([Unable to use stp/c_interface.h header])
+        ])
+
+    dnl we use [:] as a no-op so that AC_CHECK_LIB doesn't append -lstp
+    dnl automatically which would break subsequent uses of AC_CHECK_LIB()
+    STP_NEEDS_MINISAT=0
+    AC_CHECK_LIB(stp, vc_setInterfaceFlags, [:], [
+           STP_NEEDS_MINISAT=1; AC_MSG_RESULT([Could not link with libstp])
+    ], "$STP_LDFLAGS")
+    CPPFLAGS="$old_CPPFLAGS"
+
+    dnl Try linking again with minisat if necessary
+    if test "X$STP_NEEDS_MINISAT" != X0 ; then
+      # Need to clear cached result
+      unset ac_cv_lib_stp_vc_setInterfaceFlags
+
+      AC_CHECK_LIB(stp,
+               vc_setInterfaceFlags,[:], [
+               AC_MSG_ERROR([Unable to link with libstp. Check config.log to see what went wrong])
+      ], "$STP_LDFLAGS" "-lminisat" )
+
+      STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat"
+    else
+      STP_LDFLAGS="${STP_LDFLAGS} -lstp"
+    fi
+    AC_MSG_NOTICE([Using STP solver backend])
+    CPPFLAGS="$old_CPPFLAGS"
+    AC_DEFINE(ENABLE_STP, [1], [Using STP Solver backend])
 else
-  STP_LDFLAGS="${STP_LDFLAGS} -lstp"
+    AC_MSG_NOTICE([Not using STP solver backend])
 fi
 
-
+AC_SUBST(ENABLE_STP)
 AC_SUBST(STP_CFLAGS)
 AC_SUBST(STP_LDFLAGS)
 
+
 dnl **************************************************************************
-dnl User option to enable metaSMT constraint solvers and to specify the 
+dnl User option to enable metaSMT constraint solvers and to specify the
 dnl the location of the metaSMT root directory
 dnl **************************************************************************
 
@@ -613,13 +625,13 @@ AC_ARG_WITH(metasmt,
     [Location of metaSMT installation directory]),,)
 
 if test X$with_metasmt = X ; then
-  AC_SUBST(ENABLE_METASMT,[[0]])
+  ENABLE_METASMT=0
 else
   metasmt_root=`cd $with_metasmt 2> /dev/null; pwd`
 
   dnl AC_LANG(C++)
   old_CPPFLAGS="$CPPFLAGS"
-  old_LDFLAGS="$LDFLAGS"  
+  old_LDFLAGS="$LDFLAGS"
   CPPFLAGS="$CPPFLAGS -I$metasmt_root/include"
   LDFLAGS="$LDFLAGS -L$metasmt_root/lib -lmetaSMT"
   AC_CHECK_HEADERS([$metasmt_root/include/metaSMT/DirectSolver_Context.hpp $metasmt_root/include/metaSMT/frontend/QF_BV.hpp],, [
@@ -627,14 +639,24 @@ else
   ])
   AC_LINK_IFELSE(
       [AC_LANG_PROGRAM([#include $metasmt_root/include/metaSMT/frontend/QF_BV.hpp], [metaSMT::logic::QF_BV::new_bitvector(3)])],
-      [],[AC_MSG_CHECKING([for new_bitvector() in -lmetaSMT])],[AC_MSG_ERROR([Unable to link with libmetaSMT])])  
+      [],[AC_MSG_CHECKING([for new_bitvector() in -lmetaSMT])],[AC_MSG_ERROR([Unable to link with libmetaSMT])])
   CPPFLAGS="$old_CPPFLAGS"
   LDFLAGS="$old_LDFLAGS"
 
-  AC_DEFINE(SUPPORT_METASMT, 1, [Supporting metaSMT API])
-  AC_SUBST(ENABLE_METASMT,[[1]])
+  AC_DEFINE(ENABLE_METASMT, 1, [Enable metaSMT API])
   AC_SUBST(METASMT_ROOT,$metasmt_root)
   AC_SUBST(REQUIRES_RTTI,[[1]])
+  ENABLE_METASMT=1
+fi
+
+AC_SUBST(ENABLE_METASMT)
+
+dnl **************************************************************************
+dnl Check at least one solver backend is enabled
+dnl **************************************************************************
+
+if test "X$ENABLE_STP$ENABLE_METASMT" == X00 ; then
+    AC_MSG_ERROR([At least one solver backend must be enabled, try using --with-stp or --with-metasmt])
 fi
 
 
diff --git a/configure b/configure
index 72ed1883..af871ce6 100755
--- a/configure
+++ b/configure
@@ -624,10 +624,11 @@ ac_includes_default="\
 
 ac_subst_vars='LTLIBOBJS
 LIBOBJS
-METASMT_ROOT
 ENABLE_METASMT
+METASMT_ROOT
 STP_LDFLAGS
 STP_CFLAGS
+ENABLE_STP
 CXXCPP
 HAVE_SELINUX
 EGREP
@@ -4865,43 +4866,45 @@ fi
 
 
 
+ENABLE_STP=0
 
 # Check whether --with-stp was given.
 if test "${with_stp+set}" = set; then :
   withval=$with_stp;
       #Check for empty argument
       if test "X$withval" = X ; then
-	      as_fn_error $? "<path> cannot be empty in --with-stp=<path>" "$LINENO" 5
+        as_fn_error $? "<path> cannot be empty in --with-stp=<path>" "$LINENO" 5
       fi
       stp_root=`(cd $withval && pwd) 2> /dev/null`
 
       #Check for bad path
       if test "X$stp_root" = X ; then
-	    as_fn_error $? "Cannot access path $with_stp passed to --with-stp" "$LINENO" 5
+        as_fn_error $? "Cannot access path $with_stp passed to --with-stp" "$LINENO" 5
       fi
 
       STP_CFLAGS="-I$stp_root/include"
       STP_LDFLAGS="-L$stp_root/lib"
+      ENABLE_STP=1
 
 fi
 
 
-old_CPPFLAGS="$CPPFLAGS"
-CPPFLAGS="$CPPFLAGS $STP_CFLAGS"
-ac_fn_cxx_check_header_mongrel "$LINENO" "stp/c_interface.h" "ac_cv_header_stp_c_interface_h" "$ac_includes_default"
+if test "X$ENABLE_STP" != X0; then
+    old_CPPFLAGS="$CPPFLAGS"
+    CPPFLAGS="$CPPFLAGS $STP_CFLAGS"
+    ac_fn_cxx_check_header_mongrel "$LINENO" "stp/c_interface.h" "ac_cv_header_stp_c_interface_h" "$ac_includes_default"
 if test "x$ac_cv_header_stp_c_interface_h" = xyes; then :
 
 else
 
-        as_fn_error $? "Unable to use stp/c_interface.h header" "$LINENO" 5
+            as_fn_error $? "Unable to use stp/c_interface.h header" "$LINENO" 5
 
 fi
 
 
-CPPFLAGS="$old_CPPFLAGS"
 
-STP_NEEDS_MINISAT=0
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
+            STP_NEEDS_MINISAT=0
+    { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
 $as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; }
 if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then :
   $as_echo_n "(cached) " >&6
@@ -4938,25 +4941,21 @@ fi
 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5
 $as_echo "$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; }
 if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = xyes; then :
-  cat >>confdefs.h <<_ACEOF
-#define HAVE_LIBSTP 1
-_ACEOF
-
-  LIBS="-lstp $LIBS"
-
+  :
 else
 
-       STP_NEEDS_MINISAT=1; { $as_echo "$as_me:${as_lineno-$LINENO}: result: Could not link with libstp" >&5
+           STP_NEEDS_MINISAT=1; { $as_echo "$as_me:${as_lineno-$LINENO}: result: Could not link with libstp" >&5
 $as_echo "Could not link with libstp" >&6; }
 
 fi
 
+    CPPFLAGS="$old_CPPFLAGS"
 
-if test "X$STP_NEEDS_MINISAT" != X0 ; then
-  # Need to clear cached result
-  unset ac_cv_lib_stp_vc_setInterfaceFlags
+        if test "X$STP_NEEDS_MINISAT" != X0 ; then
+      # Need to clear cached result
+      unset ac_cv_lib_stp_vc_setInterfaceFlags
 
-  { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
+      { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
 $as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; }
 if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then :
   $as_echo_n "(cached) " >&6
@@ -4993,22 +4992,27 @@ fi
 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5
 $as_echo "$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; }
 if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = xyes; then :
-  cat >>confdefs.h <<_ACEOF
-#define HAVE_LIBSTP 1
-_ACEOF
-
-  LIBS="-lstp $LIBS"
-
+  :
 else
 
-	       as_fn_error $? "Unable to link with libstp. Check config.log to see what went wrong" "$LINENO" 5
+               as_fn_error $? "Unable to link with libstp. Check config.log to see what went wrong" "$LINENO" 5
 
 fi
 
 
-  STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat"
+      STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat"
+    else
+      STP_LDFLAGS="${STP_LDFLAGS} -lstp"
+    fi
+    { $as_echo "$as_me:${as_lineno-$LINENO}: Using STP solver backend" >&5
+$as_echo "$as_me: Using STP solver backend" >&6;}
+    CPPFLAGS="$old_CPPFLAGS"
+
+$as_echo "#define ENABLE_STP 1" >>confdefs.h
+
 else
-  STP_LDFLAGS="${STP_LDFLAGS} -lstp"
+    { $as_echo "$as_me:${as_lineno-$LINENO}: Not using STP solver backend" >&5
+$as_echo "$as_me: Not using STP solver backend" >&6;}
 fi
 
 
@@ -5017,6 +5021,7 @@ fi
 
 
 
+
 # Check whether --with-metasmt was given.
 if test "${with_metasmt+set}" = set; then :
   withval=$with_metasmt;
@@ -5025,7 +5030,6 @@ fi
 
 if test X$with_metasmt = X ; then
   ENABLE_METASMT=0
-
 else
   metasmt_root=`cd $with_metasmt 2> /dev/null; pwd`
 
@@ -5073,14 +5077,20 @@ rm -f core conftest.err conftest.$ac_objext \
   LDFLAGS="$old_LDFLAGS"
 
 
-$as_echo "#define SUPPORT_METASMT 1" >>confdefs.h
-
-  ENABLE_METASMT=1
+$as_echo "#define ENABLE_METASMT 1" >>confdefs.h
 
   METASMT_ROOT=$metasmt_root
 
   REQUIRES_RTTI=1
 
+  ENABLE_METASMT=1
+fi
+
+
+
+
+if test "X$ENABLE_STP$ENABLE_METASMT" == X00 ; then
+    as_fn_error $? "At least one solver backend must be enabled, try using --with-stp or --with-metasmt" "$LINENO" 5
 fi
 
 
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index 44f1afd4..dc0f135a 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -47,7 +47,7 @@ extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
 enum CoreSolverType { STP_SOLVER, METASMT_SOLVER, DUMMY_SOLVER };
 extern llvm::cl::opt<CoreSolverType> CoreSolverToUse;
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 enum MetaSMTBackendType
 {
@@ -58,7 +58,7 @@ enum MetaSMTBackendType
 
 extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
 
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
 //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions
 template <typename T>
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 978c901f..9d34e7b6 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -6,15 +6,18 @@
 /* Enable KLEE DEBUG checks */
 #undef ENABLE_KLEE_DEBUG
 
+/* Enable metaSMT API */
+#undef ENABLE_METASMT
+
+/* Using STP Solver backend */
+#undef ENABLE_STP
+
 /* Does the platform use __ctype_b_loc, etc. */
 #undef HAVE_CTYPE_EXTERNALS
 
 /* Define to 1 if you have the <inttypes.h> header file. */
 #undef HAVE_INTTYPES_H
 
-/* Define to 1 if you have the `stp' library (-lstp). */
-#undef HAVE_LIBSTP
-
 /* Define if mallinfo() is available on this platform. */
 #undef HAVE_MALLINFO
 
@@ -93,7 +96,4 @@
 /* klee-uclibc is supported */
 #undef SUPPORT_KLEE_UCLIBC
 
-/* Supporting metaSMT API */
-#undef SUPPORT_METASMT
-
 #endif
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index e3adac6a..fed6191a 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -203,6 +203,7 @@ namespace klee {
     virtual void setCoreSolverTimeout(double timeout);
   };
 
+#ifdef ENABLE_STP
   /// STPSolver - A complete solver based on STP.
   class STPSolver : public Solver {
   public:
@@ -222,9 +223,10 @@ namespace klee {
     /// is off.
     virtual void setCoreSolverTimeout(double timeout);
   };
+#endif // ENABLE_STP
 
   
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
   
   template<typename SolverContext>
   class MetaSMTSolver : public Solver {
@@ -236,7 +238,7 @@ namespace klee {
     virtual void setCoreSolverTimeout(double timeout);
 };
 
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
   /* *** */
 
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index d7157b25..2f97b200 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -73,7 +73,7 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
     llvm::cl::CommaSeparated
 );
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
     "metasmt-backend",
@@ -86,16 +86,31 @@ llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
         clEnumValEnd),
     llvm::cl::init(METASMT_BACKEND_STP));
 
-#endif /* SUPPORT_METASMT */
-
+#endif /* ENABLE_METASMT */
+
+// Pick the default core solver based on configuration
+#ifdef ENABLE_STP
+#define STP_IS_DEFAULT_STR " (default)"
+#define METASMT_IS_DEFAULT_STR ""
+#define DEFAULT_CORE_SOLVER STP_SOLVER
+#elif ENABLE_METASMT
+#define STP_IS_DEFAULT_STR ""
+#define METASMT_IS_DEFAULT_STR " (default)"
+#define DEFAULT_CORE_SOLVER METASMT_SOLVER
+#else
+#error "Unsupported solver configuration"
+#endif
 llvm::cl::opt<CoreSolverType> CoreSolverToUse(
     "solver-backend", llvm::cl::desc("Specifiy the core solver backend to use"),
-    llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp (default)"),
-                     clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"),
+    llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp" STP_IS_DEFAULT_STR),
+                     clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT" METASMT_IS_DEFAULT_STR),
                      clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
                      clEnumValEnd),
-    llvm::cl::init(STP_SOLVER));
+    llvm::cl::init(DEFAULT_CORE_SOLVER));
 }
+#undef STP_IS_DEFAULT_STR
+#undef METASMT_IS_DEFAULT_STR
+#undef DEFAULT_CORE_SOLVER
 
 
 
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index 9d21931d..0d451f27 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -13,7 +13,7 @@
 #include "llvm/Support/raw_ostream.h"
 #include <string>
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 #include <metaSMT/frontend/Array.hpp>
 #include <metaSMT/backend/Z3_Backend.hpp>
@@ -61,17 +61,22 @@ static Solver *handleMetaSMT() {
   llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
   return coreSolver;
 }
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
 namespace klee {
 
 Solver *createCoreSolver(CoreSolverType cst) {
   switch (cst) {
   case STP_SOLVER:
+#ifdef ENABLE_STP
     llvm::errs() << "Using STP solver backend\n";
     return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+#else
+    llvm::errs() << "Not compiled with STP support\n";
+    return NULL;
+#endif
   case METASMT_SOLVER:
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
     llvm::errs() << "Using MetaSMT solver backend\n";
     return handleMetaSMT();
 #else
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index 6da1b492..ffd3cfe9 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -15,7 +15,7 @@
 #include "klee/util/ExprHashMap.h"
 #include "ConstantDivision.h"
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 #include "llvm/Support/CommandLine.h"
 
@@ -1177,6 +1177,6 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
 
 }  /* end of namespace klee */
 
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
 #endif /* METASMTBUILDER_H_ */
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 8394bbf3..971ef371 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -6,8 +6,8 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-
-#ifdef SUPPORT_METASMT
+#include "klee/Config/config.h"
+#ifdef ENABLE_METASMT
 
 #include "MetaSMTBuilder.h"
 #include "klee/Constraints.h"
@@ -463,4 +463,4 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
 }
-#endif // SUPPORT_METASMT
+#endif // ENABLE_METASMT
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 2f51c2b9..2b07f391 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -6,7 +6,8 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-
+#include "klee/Config/config.h"
+#ifdef ENABLE_STP
 #include "STPBuilder.h"
 
 #include "klee/Expr.h"
@@ -902,5 +903,5 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     return vc_trueExpr(vc);
   }
 }
-
+#endif // ENABLE_STP
 
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index cb15a23c..5c49521e 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -6,7 +6,8 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-
+#include "klee/Config/config.h"
+#ifdef ENABLE_STP
 #include "STPBuilder.h"
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
@@ -382,3 +383,4 @@ void STPSolver::setCoreSolverTimeout(double timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
 }
+#endif // ENABLE_STP
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index 10b19a20..a72c4c9d 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -19,7 +19,9 @@ LINK_COMPONENTS = support
 
 include $(LEVEL)/Makefile.common
 
-LIBS += $(STP_LDFLAGS)
+ifneq ($(ENABLE_STP),0)
+  LIBS += $(STP_LDFLAGS)
+endif
 
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index f91693c5..ea9be41f 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -36,7 +36,7 @@ using namespace llvm;
 using namespace klee;
 using namespace klee::expr;
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 #include <metaSMT/DirectSolver_Context.hpp>
 #include <metaSMT/backend/Z3_Backend.hpp>
@@ -53,7 +53,7 @@ using namespace klee::expr;
 using namespace metaSMT;
 using namespace metaSMT::solver;
 
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
 
 
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index eb80d845..8e9ac6b7 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -20,7 +20,9 @@ LINK_COMPONENTS += irreader
 endif
 include $(LEVEL)/Makefile.common
 
-LIBS += $(STP_LDFLAGS)
+ifneq ($(ENABLE_STP),0)
+  LIBS += $(STP_LDFLAGS)
+endif
 
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
diff --git a/unittests/Expr/Makefile b/unittests/Expr/Makefile
index e52aea31..ca92271a 100644
--- a/unittests/Expr/Makefile
+++ b/unittests/Expr/Makefile
@@ -10,4 +10,3 @@ LINK_COMPONENTS := support
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
 CXXFLAGS += -DLLVM_29_UNITTEST
-LIBS += $(STP_LDFLAGS)
diff --git a/unittests/Ref/Makefile b/unittests/Ref/Makefile
index 14dcc8bd..10c4bebd 100644
--- a/unittests/Ref/Makefile
+++ b/unittests/Ref/Makefile
@@ -8,5 +8,3 @@ USEDLIBS := kleaverExpr.a kleeBasic.a
 LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
-
-LIBS += $(STP_LDFLAGS)
diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile
index aeac34ac..65edbe7a 100644
--- a/unittests/Solver/Makefile
+++ b/unittests/Solver/Makefile
@@ -9,4 +9,6 @@ LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
-LIBS += $(STP_LDFLAGS)
+ifneq ($(ENABLE_STP),0)
+  LIBS += $(STP_LDFLAGS)
+endif
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-21 21:53:28 +0000