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 /lib/Basic | |
| 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 'lib/Basic')
| -rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 27 |
1 files changed, 21 insertions, 6 deletions
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 |