From 79237753a1e9cbe653e5763ffd61f3cb5b8759c1 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 2 Jan 2013 15:49:34 +0000 Subject: Patch by Tomasz Kuchta adding more detailed information on query failures. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171391 91177308-0d34-0410-b5e6-96231b3b80d8 --- tools/kleaver/main.cpp | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'tools/kleaver') 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 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 > 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()) + << ")"; } } -- cgit 1.4.1