From 508d56ea83774a2af65e27ce0635840ed9898b49 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 6 Mar 2013 18:28:12 +0000 Subject: Patch by Tomek Kuchta which adds the --max-stp-time option to Kleaver. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176571 91177308-0d34-0410-b5e6-96231b3b80d8 --- tools/kleaver/main.cpp | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) (limited to 'tools') diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 6b0008db..48c24257 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -179,8 +179,18 @@ static bool EvaluateInputAST(const char *Filename, return false; // FIXME: Support choice of solver. - Solver *S, *STP = S = - UseDummySolver ? createDummySolver() : new STPSolver(true); + Solver *S = 0; + Solver *STP = 0; + if (!UseDummySolver) { + STPSolver* stpSolver = new STPSolver(true); + if (0 != MaxSTPTime) { + stpSolver->setTimeout(MaxSTPTime); + } + STP = S = stpSolver; + } + else { + STP = S = createDummySolver(); + } if (true == optionIsSet(queryLoggingOptions, SOLVER_PC)) S = createPCLoggingSolver(S, SOLVER_QUERIES_PC_FILE_NAME, MinQueryTimeToLog); if (UseFastCexSolver) @@ -252,7 +262,15 @@ static bool EvaluateInputAST(const char *Filename, std::cout << "\n"; } } else { - std::cout << "VALID (counterexample request ignored)"; + SolverImpl::SolverRunStatus retCode = S->impl->getOperationStatusCode(); + if (SolverImpl::SOLVER_RUN_STATUS_TIMEOUT == retCode) { + std::cout << " FAIL (reason: " + << SolverImpl::getOperationStatusString(retCode) + << ")"; + } + else { + std::cout << "VALID (counterexample request ignored)"; + } } } -- cgit 1.4.1