diff options
| -rw-r--r-- | lib/Module/InstructionInfoTable.cpp | 38 | ||||
| -rw-r--r-- | test/Feature/StatesCoveringNew.c | 41 |
2 files changed, 57 insertions, 22 deletions
diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp index 19d7e511..82d60708 100644 --- a/lib/Module/InstructionInfoTable.cpp +++ b/lib/Module/InstructionInfoTable.cpp @@ -34,6 +34,7 @@ #endif #include "llvm/Analysis/ValueTracking.h" #include "llvm/Support/Debug.h" +#include "llvm/Support/ErrorHandling.h" #include <map> #include <string> @@ -121,23 +122,12 @@ InstructionInfoTable::InstructionInfoTable(Module *m) lineTable.find(instr); if (ltit!=lineTable.end()) assemblyLine = ltit->second; - 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"); - } + getInstructionDebugInfo(instr, initialFile, initialLine); + infos.insert(std::make_pair(instr, + InstructionInfo(id++, + *initialFile, + initialLine, + assemblyLine))); } } } @@ -168,16 +158,20 @@ const InstructionInfo & InstructionInfoTable::getInfo(const Instruction *inst) const { std::map<const llvm::Instruction*, InstructionInfo>::const_iterator it = infos.find(inst); - if (it==infos.end()) { - return dummyInfo; - } else { - return it->second; - } + if (it == infos.end()) + llvm::report_fatal_error("invalid instruction, not present in " + "initial module!"); + return it->second; } const InstructionInfo & InstructionInfoTable::getFunctionInfo(const Function *f) const { if (f->isDeclaration()) { + // FIXME: We should probably eliminate this dummyInfo object, and instead + // allocate a per-function object to track the stats for that function + // (otherwise, anyone actually trying to use those stats is getting ones + // shared across all functions). I'd like to see if this matters in practice + // and construct a test case for it if it does, though. return dummyInfo; } else { return getInfo(f->begin()->begin()); diff --git a/test/Feature/StatesCoveringNew.c b/test/Feature/StatesCoveringNew.c new file mode 100644 index 00000000..e372e89e --- /dev/null +++ b/test/Feature/StatesCoveringNew.c @@ -0,0 +1,41 @@ +// Check that we properly detect states covering new instructions. +// +// RUN: %llvmgcc -I../../../include %s -emit-llvm -O0 -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --only-output-states-covering-new %t1.bc + +// We expect 4 different output states, one for each named value and one "other" +// one with the prefered CEX. We verify this by using ktest-tool to dump the +// values, and then checking the output. +// +// RUN: /bin/sh -c "ktest-tool --write-int %t.klee-out/*.ktest" | sort > %t.data-values +// RUN: FileCheck < %t.data-values %s + +// CHECK: object 0: data: 0 +// CHECK: object 0: data: 17 +// CHECK: object 0: data: 32 +// CHECK: object 0: data: 99 + +#include <klee/klee.h> + +void f0(void) {} +void f1(void) {} +void f2(void) {} +void f3(void) {} + +int main() { + int x = klee_range(0, 256, "x"); + + if (x == 17) { + f0(); + } else if (x == 32) { + f1(); + } else if (x == 99) { + f2(); + } else { + klee_prefer_cex(&x, x == 0); + f3(); + } + + return 0; +} |