diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/CommandLine.h | 2 | ||||
| -rw-r--r-- | include/klee/Solver.h | 6 | ||||
| -rw-r--r-- | include/klee/util/Assignment.h | 1 |
3 files changed, 9 insertions, 0 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index cc186db7..6a72692d 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -29,6 +29,8 @@ extern llvm::cl::opt<bool> UseForkedCoreSolver; extern llvm::cl::opt<bool> CoreSolverOptimizeDivides; +extern llvm::cl::opt<bool> UseAssignmentValidatingSolver; + ///The different query logging solvers that can switched on/off enum QueryLoggingSolverType { diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 2f613992..32c8cf9e 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -268,6 +268,12 @@ namespace klee { /// \param oracle - The solver to check query results against. Solver *createValidatingSolver(Solver *s, Solver *oracle); + /// createAssignmentValidatingSolver - Create a solver that when requested + /// for an assignment will check that the computed assignment satisfies + /// the Query. + /// \param s - The underlying solver to use. + Solver *createAssignmentValidatingSolver(Solver *s); + /// createCachingSolver - Create a solver which will cache the queries in /// memory (without eviction). /// diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index 5d8aa1ab..55e681de 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -46,6 +46,7 @@ namespace klee { ref<Expr> evaluate(const Array *mo, unsigned index) const; ref<Expr> evaluate(ref<Expr> e); + void createConstraintsFromAssignment(std::vector<ref<Expr> > &out) const; template<typename InputIterator> bool satisfies(InputIterator begin, InputIterator end); |