diff options
Diffstat (limited to 'lib/Core/Executor.cpp')
| -rw-r--r-- | lib/Core/Executor.cpp | 50 |
1 files changed, 40 insertions, 10 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 74769aa1..968283b7 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -32,6 +32,7 @@ #include "klee/TimerStatIncrementer.h" #include "klee/util/Assignment.h" #include "klee/util/ExprPPrinter.h" +#include "klee/util/ExprSMTLIBLetPrinter.h" #include "klee/util/ExprUtil.h" #include "klee/util/GetElementPtrTypeIterator.h" #include "klee/Config/Version.h" @@ -3373,17 +3374,46 @@ unsigned Executor::getSymbolicPathStreamID(const ExecutionState &state) { void Executor::getConstraintLog(const ExecutionState &state, std::string &res, - bool asCVC) { - if (asCVC) { - Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); - char *log = solver->stpSolver->getConstraintLog(query); - res = std::string(log); - free(log); - } else { - std::ostringstream info; - ExprPPrinter::printConstraints(info, state.constraints); - res = info.str(); + Interpreter::LogType logFormat) { + + std::ostringstream info; + + switch(logFormat) + { + case STP: + { + Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); + char *log = solver->stpSolver->getConstraintLog(query); + res = std::string(log); + free(log); + } + break; + + case KQUERY: + { + std::ostringstream info; + ExprPPrinter::printConstraints(info, state.constraints); + res = info.str(); + } + break; + + case SMTLIB2: + { + std::ostringstream info; + ExprSMTLIBPrinter* printer = createSMTLIBPrinter(); + printer->setOutput(info); + Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); + printer->setQuery(query); + printer->generateOutput(); + res = info.str(); + delete printer; } + break; + + default: + klee_warning("Executor::getConstraintLog() : Log format not supported!"); + } + } bool Executor::getSymbolicSolution(const ExecutionState &state, |