diff options
| author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-10-08 23:28:10 +0100 |
|---|---|---|
| committer | MartinNowack <martin.nowack@gmail.com> | 2018-10-16 23:00:15 +0100 |
| commit | 9d730c318aa77593d2cb6898c0b530dbec14f045 (patch) | |
| tree | 2e0a2c85c52d01d4de6a93a6cd6ca11c4852b8ee /include | |
| parent | 5b9f6d171f06c3619db20647abf2c185b4112346 (diff) | |
| download | klee-9d730c318aa77593d2cb6898c0b530dbec14f045.tar.gz | |
Small changes to comments
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/Solver.h | 2 | ||||
| -rw-r--r-- | include/klee/SolverCmdLine.h | 12 |
2 files changed, 6 insertions, 8 deletions
diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 2b80e9ec..c2a8ef1e 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -11,7 +11,7 @@ #define KLEE_SOLVER_H #include "klee/Expr.h" -#include "klee/SolverCmdLine.h" // FIXME: This is just for CoreSolverType +#include "klee/SolverCmdLine.h" #include <vector> diff --git a/include/klee/SolverCmdLine.h b/include/klee/SolverCmdLine.h index 7a122e72..19e5fae6 100644 --- a/include/klee/SolverCmdLine.h +++ b/include/klee/SolverCmdLine.h @@ -42,14 +42,12 @@ extern llvm::cl::opt<bool> CoreSolverOptimizeDivides; extern llvm::cl::opt<bool> UseAssignmentValidatingSolver; -/// The different query logging solvers that can switched on/off +/// The different query logging solvers that can be switched on/off enum QueryLoggingSolverType { - ALL_KQUERY, ///< Log all queries (un-optimised) in .kquery (KQuery) format - ALL_SMTLIB, ///< Log all queries (un-optimised) .smt2 (SMT-LIBv2) format - SOLVER_KQUERY, ///< Log queries passed to solver (optimised) in .kquery - ///< (KQuery) format - SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 - ///< (SMT-LIBv2) format + ALL_KQUERY, ///< Log all queries in .kquery (KQuery) format + ALL_SMTLIB, ///< Log all queries .smt2 (SMT-LIBv2) format + SOLVER_KQUERY, ///< Log queries passed to solver in .kquery (KQuery) format + SOLVER_SMTLIB ///< Log queries passed to solver in .smt2 (SMT-LIBv2) format }; extern llvm::cl::bits<QueryLoggingSolverType> queryLoggingOptions; |