From 6829fb93ce36afc852c97928b94ab9ad5e221aec Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 11 Dec 2013 16:23:10 +0000
Subject: Only record debug info into InstructionInfoTable if debug information
 is actually available.

In addition if doing a DEBUG build then the command line flag

-debug-only=klee_missing_debug

shows the instructions missing debug information

and

-debug-only=klee_obtained_debug

show the instructions with debug information.
---
 lib/Module/InstructionInfoTable.cpp | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

(limited to 'lib/Module')

diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp
index 204457d2..19d7e511 100644
--- a/lib/Module/InstructionInfoTable.cpp
+++ b/lib/Module/InstructionInfoTable.cpp
@@ -33,6 +33,7 @@
 #include "llvm/Analysis/DebugInfo.h"
 #endif
 #include "llvm/Analysis/ValueTracking.h"
+#include "llvm/Support/Debug.h"
 
 #include <map>
 #include <string>
@@ -120,12 +121,23 @@ InstructionInfoTable::InstructionInfoTable(Module *m)
         lineTable.find(instr);
       if (ltit!=lineTable.end())
         assemblyLine = ltit->second;
-      getInstructionDebugInfo(instr, initialFile, initialLine);
-      infos.insert(std::make_pair(instr,
-                                  InstructionInfo(id++,
-                                                  *initialFile,
-                                                  initialLine,
-                                                  assemblyLine)));
+      if (getInstructionDebugInfo(instr, initialFile, initialLine))
+      {
+        infos.insert(std::make_pair(instr,
+                                    InstructionInfo(id++,
+                                                    *initialFile,
+                                                    initialLine,
+                                                    assemblyLine)));
+        DEBUG_WITH_TYPE("klee_obtained_debug", dbgs() <<
+          "Instruction: \"" << *instr << "\" (assembly line " << assemblyLine <<
+          ") has debug location " << *initialFile << ":" << initialLine << "\n");
+      }
+      else
+      {
+        DEBUG_WITH_TYPE("klee_missing_debug", dbgs() <<
+          "Instruction: \"" << *instr << "\" (assembly line " << assemblyLine <<
+          ") is missing debug info.\n");
+      }
     }
   }
 }
-- 
cgit 1.4.1