diff options
Diffstat (limited to 'tools/kleaver/main.cpp')
| -rw-r--r-- | tools/kleaver/main.cpp | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 16a0ea42..1a4663a1 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -8,6 +8,7 @@ #include "klee/Expr.h" #include "klee/ExprBuilder.h" #include "klee/Solver.h" +#include "klee/SolverImpl.h" #include "klee/Statistics.h" #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprVisitor.h" @@ -93,7 +94,7 @@ namespace { UseFastCexSolver("use-fast-cex-solver", cl::init(false)); - // FIXME: Command line argument duplicated in Executor.cpp of Klee. Different + // FIXME: Command line argument modified in Executor.cpp of Klee. Different // output file name used. cl::opt<bool> UseSTPQueryPCLog("use-stp-query-pc-log", @@ -220,7 +221,9 @@ static bool EvaluateInputAST(const char *Filename, result)) { std::cout << (result ? "VALID" : "INVALID"); } else { - std::cout << "FAIL"; + std::cout << "FAIL (reason: " + << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode()) + << ")"; } } else if (!QC->Values.empty()) { assert(QC->Objects.empty() && @@ -236,7 +239,9 @@ static bool EvaluateInputAST(const char *Filename, std::cout << "INVALID\n"; std::cout << "\tExpr 0:\t" << result; } else { - std::cout << "FAIL"; + std::cout << "FAIL (reason: " + << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode()) + << ")"; } } else { std::vector< std::vector<unsigned char> > result; @@ -260,7 +265,9 @@ static bool EvaluateInputAST(const char *Filename, std::cout << "\n"; } } else { - std::cout << "FAIL"; + std::cout << "FAIL (reason: " + << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode()) + << ")"; } } |