diff options
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/CommandLine.h | 14 | ||||
-rw-r--r-- | include/klee/Config/config.h.in | 3 | ||||
-rw-r--r-- | include/klee/Internal/Support/FloatEvaluation.h | 2 | ||||
-rw-r--r-- | include/klee/Solver.h | 15 | ||||
-rw-r--r-- | include/klee/util/GetElementPtrTypeIterator.h | 12 |
5 files changed, 43 insertions, 3 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index 38b22c6f..c4c70069 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -7,6 +7,7 @@ #define KLEE_COMMANDLINE_H #include "llvm/Support/CommandLine.h" +#include "klee/Config/config.h" namespace klee { @@ -43,6 +44,19 @@ enum QueryLoggingSolverType */ extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions; +#ifdef SUPPORT_METASMT + +enum MetaSMTBackendType +{ + METASMT_BACKEND_NONE, + METASMT_BACKEND_STP, + METASMT_BACKEND_Z3, + METASMT_BACKEND_BOOLECTOR +}; + +extern llvm::cl::opt<klee::MetaSMTBackendType> UseMetaSMT; + +#endif /* SUPPORT_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 4ce9714d..a751bc07 100644 --- a/include/klee/Config/config.h.in +++ b/include/klee/Config/config.h.in @@ -78,4 +78,7 @@ /* Define to 1 if you have the ANSI C header files. */ #undef STDC_HEADERS +/* Supporting metaSMT API */ +#undef SUPPORT_METASMT + #endif diff --git a/include/klee/Internal/Support/FloatEvaluation.h b/include/klee/Internal/Support/FloatEvaluation.h index 1d305374..f1f16c5e 100644 --- a/include/klee/Internal/Support/FloatEvaluation.h +++ b/include/klee/Internal/Support/FloatEvaluation.h @@ -17,6 +17,8 @@ #include "llvm/Support/MathExtras.h" +#include <cassert> + namespace klee { namespace floats { diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 8fe33c7c..00e4c962 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -219,6 +219,21 @@ namespace klee { virtual void setCoreSolverTimeout(double timeout); }; + +#ifdef SUPPORT_METASMT + + template<typename SolverContext> + class MetaSMTSolver : public Solver { + public: + MetaSMTSolver(bool useForked, bool optimizeDivides); + virtual ~MetaSMTSolver(); + + virtual char *getConstraintLog(const Query&); + virtual void setCoreSolverTimeout(double timeout); +}; + +#endif /* SUPPORT_METASMT */ + /* *** */ /// createValidatingSolver - Create a solver which will validate all query diff --git a/include/klee/util/GetElementPtrTypeIterator.h b/include/klee/util/GetElementPtrTypeIterator.h index 4446914d..2d145cd6 100644 --- a/include/klee/util/GetElementPtrTypeIterator.h +++ b/include/klee/util/GetElementPtrTypeIterator.h @@ -18,15 +18,21 @@ #ifndef KLEE_UTIL_GETELEMENTPTRTYPE_H #define KLEE_UTIL_GETELEMENTPTRTYPE_H -#include "klee/Config/Version.h" - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/User.h" +#include "llvm/IR/DerivedTypes.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/Constants.h" +#else #include "llvm/User.h" #include "llvm/DerivedTypes.h" #include "llvm/Instructions.h" -#include "klee/Config/Version.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0) #include "llvm/Constants.h" #endif +#endif + +#include "klee/Config/Version.h" namespace klee { template<typename ItTy = llvm::User::const_op_iterator> |