From bd7e31b6b6ffb5e267af403007d5b8012fdec397 Mon Sep 17 00:00:00 2001 From: Jiri Slaby Date: Fri, 22 Jul 2016 13:47:07 +0200 Subject: klee: add exit-on-error-type parameter It allows stopping the execution on some conditions like assertions. The use is like: klee -exit-on-error-type=Assert -exit-on-error-type=External file.llvm This is especially useful in the SV-COMP. A test to cover the new parameter was added too. Signed-off-by: Jiri Slaby --- lib/Core/SpecialFunctionHandler.cpp | 44 +++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 24 deletions(-) (limited to 'lib/Core/SpecialFunctionHandler.cpp') diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index caec5e39..b44b0e1b 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -273,7 +273,7 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state, KInstruction *target, std::vector > &arguments) { assert(arguments.size()==0 && "invalid number of arguments to abort"); - executor.terminateStateOnError(state, "abort failure", "abort.err"); + executor.terminateStateOnError(state, "abort failure", Executor::Abort); } void SpecialFunctionHandler::handleExit(ExecutionState &state, @@ -310,7 +310,7 @@ void SpecialFunctionHandler::handleAssert(ExecutionState &state, assert(arguments.size()==3 && "invalid number of arguments to _assert"); executor.terminateStateOnError(state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), - "assert.err"); + Executor::Assert); } void SpecialFunctionHandler::handleAssertFail(ExecutionState &state, @@ -319,7 +319,7 @@ void SpecialFunctionHandler::handleAssertFail(ExecutionState &state, assert(arguments.size()==4 && "invalid number of arguments to __assert_fail"); executor.terminateStateOnError(state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), - "assert.err"); + Executor::Assert); } void SpecialFunctionHandler::handleReportError(ExecutionState &state, @@ -330,6 +330,7 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state, // arguments[0], arguments[1] are file, line executor.terminateStateOnError(state, readStringAtAddress(state, arguments[2]), + Executor::ReportError, readStringAtAddress(state, arguments[3]).c_str()); } @@ -402,7 +403,7 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, } else { executor.terminateStateOnError(state, "invalid klee_assume call (provably false)", - "user.err"); + Executor::User); } } else { executor.addConstraint(state, e); @@ -467,7 +468,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state, } else { executor.terminateStateOnError(state, "klee_set_forking requires a constant arg", - "user.err"); + Executor::User); } } @@ -623,14 +624,14 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, if (!isa(address) || !isa(size)) { executor.terminateStateOnError(state, "check_memory_access requires constant args", - "user.err"); + Executor::User); } else { ObjectPair op; if (!state.addressSpace.resolveOne(cast(address), op)) { executor.terminateStateOnError(state, "check_memory_access: memory error", - "ptr.err", + Executor::Ptr, NULL, executor.getAddressInfo(state, address)); } else { ref chk = @@ -639,7 +640,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, if (!chk->isTrue()) { executor.terminateStateOnError(state, "check_memory_access: memory error", - "ptr.err", + Executor::Ptr, NULL, executor.getAddressInfo(state, address)); } } @@ -700,9 +701,8 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, ExecutionState *s = it->second; if (old->readOnly) { - executor.terminateStateOnError(*s, - "cannot make readonly object symbolic", - "user.err"); + executor.terminateStateOnError(*s, "cannot make readonly object symbolic", + Executor::User); return; } @@ -721,7 +721,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, } else { executor.terminateStateOnError(*s, "wrong size given to klee_make_symbolic[_name]", - "user.err"); + Executor::User); } } } @@ -746,31 +746,27 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state, void SpecialFunctionHandler::handleAddOverflow(ExecutionState &state, KInstruction *target, std::vector > &arguments) { - executor.terminateStateOnError(state, - "overflow on unsigned addition", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on unsigned addition", + Executor::Overflow); } void SpecialFunctionHandler::handleSubOverflow(ExecutionState &state, KInstruction *target, std::vector > &arguments) { - executor.terminateStateOnError(state, - "overflow on unsigned subtraction", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on unsigned subtraction", + Executor::Overflow); } void SpecialFunctionHandler::handleMulOverflow(ExecutionState &state, KInstruction *target, std::vector > &arguments) { - executor.terminateStateOnError(state, - "overflow on unsigned multiplication", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on unsigned multiplication", + Executor::Overflow); } void SpecialFunctionHandler::handleDivRemOverflow(ExecutionState &state, KInstruction *target, std::vector > &arguments) { - executor.terminateStateOnError(state, - "overflow on division or remainder", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on division or remainder", + Executor::Overflow); } -- cgit 1.4.1