diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2013-12-11 16:23:10 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2013-12-19 15:45:03 +0000 |
| commit | 6829fb93ce36afc852c97928b94ab9ad5e221aec (patch) | |
| tree | 1df5c0d413521db4b790c65877fa8a74dc98d0f1 /lib/Module | |
| parent | 58de8cdce75bcee981ec813c57fb2ed7e83e9878 (diff) | |
| download | klee-6829fb93ce36afc852c97928b94ab9ad5e221aec.tar.gz | |
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.
Diffstat (limited to 'lib/Module')
| -rw-r--r-- | lib/Module/InstructionInfoTable.cpp | 24 |
1 files changed, 18 insertions, 6 deletions
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"); + } } } } |