diff options
| -rw-r--r-- | include/klee/Solver/Solver.h | 2 | ||||
| -rw-r--r-- | lib/Solver/ConstructSolverChain.cpp | 2 | ||||
| -rw-r--r-- | lib/Solver/ValidatingSolver.cpp | 18 |
3 files changed, 14 insertions, 8 deletions
diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h index 263f1626..a2256028 100644 --- a/include/klee/Solver/Solver.h +++ b/include/klee/Solver/Solver.h @@ -221,7 +221,7 @@ namespace klee { /// /// \param s - The primary underlying solver to use. /// \param oracle - The solver to check query results against. - Solver *createValidatingSolver(Solver *s, Solver *oracle); + Solver *createValidatingSolver(Solver *s, Solver *oracle, bool ownsOracle = false); /// createAssignmentValidatingSolver - Create a solver that when requested /// for an assignment will check that the computed assignment satisfies diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp index 3dab0361..999edda4 100644 --- a/lib/Solver/ConstructSolverChain.cpp +++ b/lib/Solver/ConstructSolverChain.cpp @@ -71,7 +71,7 @@ Solver *constructSolverChain(Solver *coreSolver, } if (DebugCrossCheckCoreSolverWith != NO_SOLVER) { Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith); - solver = createValidatingSolver(/*s=*/solver, /*oracle=*/oracleSolver); + solver = createValidatingSolver(solver, oracleSolver, true); } return solver; diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp index 5d4dab39..d95b8942 100644 --- a/lib/Solver/ValidatingSolver.cpp +++ b/lib/Solver/ValidatingSolver.cpp @@ -18,18 +18,24 @@ namespace klee { class ValidatingSolver : public SolverImpl { private: Solver *solver, *oracle; + bool ownsOracle; public: - ValidatingSolver(Solver *_solver, Solver *_oracle) - : solver(_solver), oracle(_oracle) {} - ~ValidatingSolver() { delete solver; } + ValidatingSolver(Solver *solver, Solver *oracle, bool ownsOracle = false) + : solver(solver), oracle(oracle), ownsOracle(ownsOracle) {} + ~ValidatingSolver() { + delete solver; + if (ownsOracle) { + delete oracle; + } + } bool computeValidity(const Query &, Solver::Validity &result); bool computeTruth(const Query &, bool &isValid); bool computeValue(const Query &, ref<Expr> &result); bool computeInitialValues(const Query &, const std::vector<const Array *> &objects, - std::vector<std::vector<unsigned char> > &values, + std::vector<std::vector<unsigned char>> &values, bool &hasSolution); SolverRunStatus getOperationStatusCode(); char *getConstraintLog(const Query &); @@ -136,7 +142,7 @@ void ValidatingSolver::setCoreSolverTimeout(time::Span timeout) { solver->impl->setCoreSolverTimeout(timeout); } -Solver *createValidatingSolver(Solver *s, Solver *oracle) { - return new Solver(new ValidatingSolver(s, oracle)); +Solver *createValidatingSolver(Solver *s, Solver *oracle, bool ownsOracle) { + return new Solver(new ValidatingSolver(s, oracle, ownsOracle)); } } |