3 files changed, 60 insertions, 11 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index ef55f21f..f01fa4ee 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2729,16 +2729,54 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
   terminateState(state);
 }
 
+const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const ExecutionState &state,
+    Instruction ** lastInstruction) {
+  // unroll the stack of the applications state and find
+  // the last instruction which is not inside a KLEE internal function
+  ExecutionState::stack_ty::const_reverse_iterator it = state.stack.rbegin(),
+      itE = state.stack.rend();
+
+  // don't check beyond the outermost function (i.e. main())
+  itE--;
+
+  const InstructionInfo * ii = 0;
+  if (kmodule->internalFunctions.count(it->kf->function) == 0){
+    ii =  state.prevPC->info;
+    *lastInstruction = state.prevPC->inst;
+  }
+
+  // wind up the stack and check if we are in a KLEE internal function
+  for (;it != itE; ++it) {
+    // check calling instruction and if it is contained in a KLEE internal function
+    const Function * f = (*it->caller).inst->getParent()->getParent();
+    if (kmodule->internalFunctions.count(f)){
+      ii = 0;
+      continue;
+    }
+    if (!ii){
+      ii = (*it->caller).info;
+      *lastInstruction = (*it->caller).inst;
+    }
+  }
+
+  if (!ii) {
+    // something went wrong, play safe and return the current instruction info
+    *lastInstruction = state.prevPC->inst;
+    return *state.prevPC->info;
+  }
+  return *ii;
+}
 void Executor::terminateStateOnError(ExecutionState &state,
                                      const llvm::Twine &messaget,
                                      const char *suffix,
                                      const llvm::Twine &info) {
   std::string message = messaget.str();
   static std::set< std::pair<Instruction*, std::string> > emittedErrors;
-  const InstructionInfo &ii = *state.prevPC->info;
+  Instruction * lastInst;
+  const InstructionInfo &ii = getLastNonKleeInternalInstruction(state, &lastInst);
   
   if (EmitAllErrors ||
-      emittedErrors.insert(std::make_pair(state.prevPC->inst, message)).second) {
+      emittedErrors.insert(std::make_pair(lastInst, message)).second) {
     if (ii.file != "") {
       klee_message("ERROR: %s:%d: %s", ii.file.c_str(), ii.line, message.c_str());
     } else {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index b7318a2c..7d82332c 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -340,6 +340,11 @@ private:
   /// Get textual information regarding a memory address.
   std::string getAddressInfo(ExecutionState &state, ref<Expr> address) const;
 
+  // Determines the \param lastInstruction of the \param state which is not KLEE
+  // internal and returns its InstructionInfo
+  const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state,
+      llvm::Instruction** lastInstruction);
+
   // remove state from queue and delete
   void terminateState(ExecutionState &state);
   // call exit handler and terminate state
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index d889b51f..4bc10604 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -269,6 +269,17 @@ static void inlineChecks(Module *module, const char * functionName) {
     DEBUG( klee_message("Tried to inline calls to %s. %u successes, %u failures",functionName, successCount, failCount) );
 }
 
+void KModule::addInternalFunction(const char* functionName){
+  Function* internalFunction = module->getFunction(functionName);
+  if (!internalFunction) {
+    DEBUG_WITH_TYPE("KModule", klee_warning(
+        "Failed to add internal function %s. Not found.", functionName));
+    return ;
+  }
+  DEBUG( klee_message("Added function %s.",functionName));
+  internalFunctions.insert(internalFunction);
+}
+
 void KModule::prepare(const Interpreter::ModuleOptions &opts,
                       InterpreterHandler *ih) {
   if (!MergeAtExit.empty()) {
@@ -374,17 +385,12 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
 #endif
   module = linkWithLibrary(module, path.c_str());
 
-  /* In order for KLEE to report ALL errors at instrumented
-   * locations the instrumentation call (e.g. "klee_div_zero_check")
-   * must be inlined. Otherwise one of the instructions in the
-   * instrumentation function will be used as the the location of
-   * the error which means that the error cannot be recorded again
-   * ( unless -emit-all-errors is used).
-   */
+  // Add internal functions which are not used to check if instructions
+  // have been already visited
   if (opts.CheckDivZero)
-    inlineChecks(module, "klee_div_zero_check");
+    addInternalFunction("klee_div_zero_check");
   if (opts.CheckOvershift)
-    inlineChecks(module, "klee_overshift_check");
+    addInternalFunction("klee_overshift_check");
 
 
   // Needs to happen after linking (since ctors/dtors can be modified)