diff options
author | Andrea Mattavelli <andreamattavelli@users.noreply.github.com> | 2017-03-03 18:34:19 +0000 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-03-03 18:34:19 +0000 |
commit | 2b053eeded2688c7bb17be191b45c11080b44ca7 (patch) | |
tree | 882ca015f3b307f31ae34f66e3f72f7b0423e39b /lib | |
parent | 4b199e1726ac45227f62ae0365063236a9a10033 (diff) | |
parent | 6f20f660ab2ae28ba6ec8e5262a2d1c31e0ab9ed (diff) | |
download | klee-2b053eeded2688c7bb17be191b45c11080b44ca7.tar.gz |
Merge pull request #613 from ccadar/minor2
Moved printFileLine() to be part of KInstruction
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 16 | ||||
-rw-r--r-- | lib/Module/KInstruction.cpp | 7 |
2 files changed, 12 insertions, 11 deletions
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]"; +} |