about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp32
-rw-r--r--lib/Core/ExternalDispatcher.cpp3
2 files changed, 17 insertions, 18 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index c5d294fb..95812dd7 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -976,14 +976,18 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
     falseState->ptreeNode = res.first;
     trueState->ptreeNode = res.second;
 
-    if (!isInternal) {
-      if (pathWriter) {
-        falseState->pathOS = pathWriter->open(current.pathOS);
+    if (pathWriter) {
+      // Need to update the pathOS.id field of falseState, otherwise the same id
+      // is used for both falseState and trueState.
+      falseState->pathOS = pathWriter->open(current.pathOS);
+      if (!isInternal) {
         trueState->pathOS << "1";
         falseState->pathOS << "0";
-      }      
-      if (symPathWriter) {
-        falseState->symPathOS = symPathWriter->open(current.symPathOS);
+      }
+    }
+    if (symPathWriter) {
+      falseState->symPathOS = symPathWriter->open(current.symPathOS);
+      if (!isInternal) {
         trueState->symPathOS << "1";
         falseState->symPathOS << "0";
       }
@@ -1235,8 +1239,11 @@ void Executor::printDebugInstructions(ExecutionState &state) {
     stream = &debugLogBuffer;
 
   if (!optionIsSet(DebugPrintInstructions, STDERR_COMPACT) &&
-      !optionIsSet(DebugPrintInstructions, FILE_COMPACT))
-    printFileLine(state, state.pc, *stream);
+      !optionIsSet(DebugPrintInstructions, FILE_COMPACT)) {
+    (*stream) << "     ";
+    state.pc->printFileLine(*stream);
+    (*stream) << ":";
+  }
 
   (*stream) << state.pc->info->id;
 
@@ -1461,15 +1468,6 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src,
   }
 }
 
-void Executor::printFileLine(ExecutionState &state, KInstruction *ki,
-                             llvm::raw_ostream &debugFile) {
-  const InstructionInfo &ii = *ki->info;
-  if (ii.file != "")
-    debugFile << "     " << ii.file << ":" << ii.line << ":";
-  else
-    debugFile << "     [no debug info]:";
-}
-
 /// Compute the true target of a function call, resolving LLVM and KLEE aliases
 /// and bitcasts.
 Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) {
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index 01c5f935..984e3ab2 100644
--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
@@ -207,10 +207,11 @@ Function *ExternalDispatcher::createDispatcher(Function *target, Instruction *in
 
   std::vector<LLVM_TYPE_Q Type*> nullary;
   
+  // MCJIT functions need unique names, or wrong function can be called
   Function *dispatcher = Function::Create(FunctionType::get(Type::getVoidTy(ctx),
 							    nullary, false),
 					  GlobalVariable::ExternalLinkage, 
-					  "",
+					  "dispatcher_" + target->getName().str(),
 					  dispatchModule);