diff options
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 */ |