diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2013-03-11 17:11:06 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2013-03-11 17:11:06 +0000 |
| commit | 454dfc67045fbbc3358b28f855f3af0af31daf47 (patch) | |
| tree | 103a8f9d03a6fa38e111addc0e5e0015d943646b /include | |
| parent | d33011aea4f2603c1413dddc5937eca5f6091f1b (diff) | |
| download | klee-454dfc67045fbbc3358b28f855f3af0af31daf47.tar.gz | |
Patch by Dan Liew which unifies the solver construction between KLEE
and Kleaver and fixes --use-query-log in Kleaver. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176811 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/CommandLine.h | 2 | ||||
| -rw-r--r-- | include/klee/Common.h | 18 |
2 files changed, 15 insertions, 5 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index bcb490cf..f303ae6c 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -17,6 +17,8 @@ extern llvm::cl::opt<bool> UseCexCache; extern llvm::cl::opt<bool> UseCache; extern llvm::cl::opt<bool> UseIndependentSolver; + +extern llvm::cl::opt<bool> DebugValidateSolver; extern llvm::cl::opt<int> MinQueryTimeToLog; diff --git a/include/klee/Common.h b/include/klee/Common.h index 657b9341..1418f1b6 100644 --- a/include/klee/Common.h +++ b/include/klee/Common.h @@ -13,15 +13,23 @@ #ifndef KLEE_COMMON_H #define KLEE_COMMON_H +#include "klee/Solver.h" +#include <string> namespace klee { + const char ALL_QUERIES_SMT2_FILE_NAME[]="all-queries.smt2"; + const char SOLVER_QUERIES_SMT2_FILE_NAME[]="solver-queries.smt2"; + const char ALL_QUERIES_PC_FILE_NAME[]="all-queries.pc"; + const char SOLVER_QUERIES_PC_FILE_NAME[]="solver-queries.pc"; -#define ALL_QUERIES_SMT2_FILE_NAME "all-queries.smt2" -#define SOLVER_QUERIES_SMT2_FILE_NAME "solver-queries.smt2" -#define ALL_QUERIES_PC_FILE_NAME "all-queries.pc" -#define SOLVER_QUERIES_PC_FILE_NAME "solver-queries.pc" - + Solver *constructSolverChain(STPSolver *stpSolver, + std::string querySMT2LogPath, + std::string baseSolverQuerySMT2LogPath, + std::string queryPCLogPath, + std::string baseSolverQueryPCLogPath); } + + #endif /* KLEE_COMMON_H */ |