about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
Diffstat (limited to 'include')
-rw-r--r--include/klee/CommandLine.h14
-rw-r--r--include/klee/Config/config.h.in3
-rw-r--r--include/klee/Internal/Support/FloatEvaluation.h2
-rw-r--r--include/klee/Solver.h15
-rw-r--r--include/klee/util/GetElementPtrTypeIterator.h12
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>