Skip to content

Commit 0a80185

Browse files
Columpiomisonijnik
authored andcommitted
[fix] Halt when LLVM passes already proved unreachability
1 parent 0cb981d commit 0a80185

File tree

1 file changed

+13
-8
lines changed

1 file changed

+13
-8
lines changed

lib/Core/Executor.cpp

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -6672,14 +6672,19 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv,
66726672
} else {
66736673
/* Find all calls to function specified in .prp file
66746674
* and combine them to single target forest */
6675-
KFunction *kEntryFunction = kmodule->functionMap.at(f);
6676-
ref<TargetForest> forest = new TargetForest(kEntryFunction);
6677-
auto kfunction = kmodule->functionNameMap.at(FunctionCallReproduce);
6678-
KBlock *kCallBlock = kfunction->entryKBlock;
6679-
forest->add(ReproduceErrorTarget::create(
6680-
{ReachWithError::Reachable}, "",
6681-
ErrorLocation(kCallBlock->getFirstInstruction()), kCallBlock));
6682-
prepTargets.emplace(kEntryFunction, forest);
6675+
auto kfIt = kmodule->functionNameMap.find(FunctionCallReproduce);
6676+
if (kfIt == kmodule->functionNameMap.end()) {
6677+
klee_warning("%s was eliminated by LLVM passes, so it is unreachable",
6678+
FunctionCallReproduce.c_str());
6679+
} else {
6680+
auto kCallBlock = kfIt->second->entryKBlock;
6681+
KFunction *kEntryFunction = kmodule->functionMap.at(f);
6682+
ref<TargetForest> forest = new TargetForest(kEntryFunction);
6683+
forest->add(ReproduceErrorTarget::create(
6684+
{ReachWithError::Reachable}, "",
6685+
ErrorLocation(kCallBlock->getFirstInstruction()), kCallBlock));
6686+
prepTargets.emplace(kEntryFunction, forest);
6687+
}
66836688
}
66846689

66856690
if (prepTargets.empty()) {

0 commit comments

Comments
 (0)