From ee5a905cda1af731c3994e63f140c654c5dc7c2c Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Fri, 4 Dec 2015 18:55:24 -0600 Subject: Add command line flag ``--silent-klee-assume``to suppress errors due to infeasible assumptions. --- lib/Core/SpecialFunctionHandler.cpp | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'lib/Core') diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 52abff5f..8befe8f6 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -42,6 +42,11 @@ namespace { cl::init(false), cl::desc("Prefer creation of POSIX inputs (command-line arguments, files, etc.) with human readable bytes. " "Note: option is expensive when creating lots of tests (default=false)")); + + cl::opt + SilentKleeAssume("silent-klee-assume", + cl::init(false), + cl::desc("Do not treat infeasible assumption as error.")); } @@ -391,9 +396,13 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, bool success __attribute__ ((unused)) = executor.solver->mustBeFalse(state, e, res); assert(success && "FIXME: Unhandled solver failure"); if (res) { - executor.terminateStateOnError(state, - "invalid klee_assume call (provably false)", - "user.err"); + if (SilentKleeAssume) { + executor.terminateState(state); + } else { + executor.terminateStateOnError(state, + "invalid klee_assume call (provably false)", + "user.err"); + } } else { executor.addConstraint(state, e); } -- cgit 1.4.1