Merge pull request #613 from ccadar/minor2

Moved printFileLine() to be part of KInstruction

3 files changed, 19 insertions, 12 deletions

diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h
index 62f514ff..1cad98fd 100644
--- a/include/klee/Internal/Module/KInstruction.h
+++ b/include/klee/Internal/Module/KInstruction.h
@@ -11,7 +11,11 @@
 #define KLEE_KINSTRUCTION_H
 
 #include "klee/Config/Version.h"
+#include "klee/Internal/Module/InstructionInfoTable.h"
+
 #include "llvm/Support/DataTypes.h"
+#include "llvm/Support/raw_ostream.h"
+
 #include <vector>
 
 namespace llvm {
@@ -39,7 +43,9 @@ namespace klee {
     unsigned dest;
 
   public:
-    virtual ~KInstruction(); 
+    virtual ~KInstruction();
+    void printFileLine(llvm::raw_ostream &);
+
   };
 
   struct KGEPInstruction : KInstruction {
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index f5b46fc0..95812dd7 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1239,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;
 
@@ -1465,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/Module/KInstruction.cpp b/lib/Module/KInstruction.cpp
index 799620c6..a32745b8 100644
--- a/lib/Module/KInstruction.cpp
+++ b/lib/Module/KInstruction.cpp
@@ -17,3 +17,10 @@ using namespace klee;
 KInstruction::~KInstruction() {
   delete[] operands;
 }
+
+void KInstruction::printFileLine(llvm::raw_ostream &debugFile) {
+  if (info->file != "")
+    debugFile << info->file << ":" << info->line;
+  else
+    debugFile << "[no debug info]";
+}