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.

1 files changed, 3 insertions, 1 deletions

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<InvokeInst>(i))