From 3f14e3f225c442ba8c274214c5dad3195d5cb7c3 Mon Sep 17 00:00:00 2001 From: Alastair Reid Date: Wed, 12 Aug 2020 10:36:46 +0000 Subject: More robust handling of unknown intrinsics - If an unknown intrinsic appears in the bitcode file, it is reported but execution can proceed. - If an unknown intrinsic is encountered during execution of some path, - the intrinsic is reported - this path is treated as an error - execution of other paths can proceed To be more precise, there is a list of "known unknown intrinsics". Intrinsics not on this list will prevent execution. --- lib/Core/Executor.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'lib/Core') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 3dbb5a66..ea3fffb7 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1511,7 +1511,9 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, // FIXME: It would be nice to check for errors in the usage of this as // well. default: - klee_error("unknown intrinsic: %s", f->getName().data()); + klee_warning("unimplemented intrinsic: %s", f->getName().data()); + terminateStateOnError(state, "unimplemented intrinsic", Unhandled); + return; } if (InvokeInst *ii = dyn_cast(i)) -- cgit 1.4.1