diff options
| -rw-r--r-- | include/klee/MergeHandler.h | 3 | ||||
| -rw-r--r-- | lib/Core/MergeHandler.cpp | 6 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 2 |
3 files changed, 4 insertions, 7 deletions
diff --git a/include/klee/MergeHandler.h b/include/klee/MergeHandler.h index 75f4a3d1..213264e6 100644 --- a/include/klee/MergeHandler.h +++ b/include/klee/MergeHandler.h @@ -133,9 +133,6 @@ public: /// @brief Remove state from the 'openStates' vector void removeOpenState(ExecutionState *es); - /// @brief Remove state from the 'inCloseMerge' set in the executor - void removeFromCloseMergeSet(ExecutionState *es); - /// @brief True, if any states have run into 'klee_close_merge()' and have /// not been released yet bool hasMergedStates(); diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp index 67c24912..d3a6b59d 100644 --- a/lib/Core/MergeHandler.cpp +++ b/lib/Core/MergeHandler.cpp @@ -69,10 +69,6 @@ void MergeHandler::removeOpenState(ExecutionState *es){ openStates.pop_back(); } -void MergeHandler::removeFromCloseMergeSet(ExecutionState *es){ - executor->inCloseMerge.erase(es); -} - void MergeHandler::addClosedState(ExecutionState *es, llvm::Instruction *mp) { // Update stats @@ -102,6 +98,7 @@ void MergeHandler::addClosedState(ExecutionState *es, for (auto& mState: cpv) { if (mState->merge(*es)) { executor->terminateState(*es); + executor->inCloseMerge.erase(es); mergedSuccessful = true; break; } @@ -117,6 +114,7 @@ void MergeHandler::releaseStates() { for (auto& curMergeGroup: reachedCloseMerge) { for (auto curState: curMergeGroup.second) { executor->continueState(*curState); + executor->inCloseMerge.erase(curState); } } reachedCloseMerge.clear(); diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 22c27432..d85c5e93 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -375,6 +375,8 @@ void SpecialFunctionHandler::handleCloseMerge(ExecutionState &state, warning << &state << " ran into a close at " << i << " without a preceding open"; klee_warning("%s", warning.str().c_str()); } else { + assert(executor.inCloseMerge.find(&state) == executor.inCloseMerge.end() && + "State cannot run into close_merge while being closed"); executor.inCloseMerge.insert(&state); state.openMergeStack.back()->addClosedState(&state, i); state.openMergeStack.pop_back(); |