diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-12-12 20:14:01 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-01-14 11:50:09 +0000 |
| commit | 8a7705ad979096d4e611fb2b8b397c48dd5fffc1 (patch) | |
| tree | 86a2fd486e2bca162d4b4f3aa0d3b90927f76e1d /include | |
| parent | e81f5ceed580d4d267e3c857b47637d6bd065499 (diff) | |
| download | klee-8a7705ad979096d4e611fb2b8b397c48dd5fffc1.tar.gz | |
Make it possible to build KLEE without using STP and only MetaSMT.
The default core solver is STP if KLEE is built with STP otherwise it is MetaSMT. Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for consistency.
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/CommandLine.h | 4 | ||||
| -rw-r--r-- | include/klee/Config/config.h.in | 12 | ||||
| -rw-r--r-- | include/klee/Solver.h | 6 |
3 files changed, 12 insertions, 10 deletions
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 */ /* *** */ |