|
@@ -675,44 +675,35 @@ void ExprEngine::removeDead(ExplodedNode *Pred, ExplodedNodeSet &Out,
|
|
|
// Process any special transfer function for dead symbols.
|
|
|
// A tag to track convenience transitions, which can be removed at cleanup.
|
|
|
static SimpleProgramPointTag cleanupTag(TagProviderName, "Clean Node");
|
|
|
- if (!SymReaper.hasDeadSymbols()) {
|
|
|
- // Generate a CleanedNode that has the environment and store cleaned
|
|
|
- // up. Since no symbols are dead, we can optimize and not clean out
|
|
|
- // the constraint manager.
|
|
|
- StmtNodeBuilder Bldr(Pred, Out, *currBldrCtx);
|
|
|
- Bldr.generateNode(DiagnosticStmt, Pred, CleanedState, &cleanupTag, K);
|
|
|
-
|
|
|
- } else {
|
|
|
- // Call checkers with the non-cleaned state so that they could query the
|
|
|
- // values of the soon to be dead symbols.
|
|
|
- ExplodedNodeSet CheckedSet;
|
|
|
- getCheckerManager().runCheckersForDeadSymbols(CheckedSet, Pred, SymReaper,
|
|
|
- DiagnosticStmt, *this, K);
|
|
|
-
|
|
|
- // For each node in CheckedSet, generate CleanedNodes that have the
|
|
|
- // environment, the store, and the constraints cleaned up but have the
|
|
|
- // user-supplied states as the predecessors.
|
|
|
- StmtNodeBuilder Bldr(CheckedSet, Out, *currBldrCtx);
|
|
|
- for (const auto I : CheckedSet) {
|
|
|
- ProgramStateRef CheckerState = I->getState();
|
|
|
-
|
|
|
- // The constraint manager has not been cleaned up yet, so clean up now.
|
|
|
- CheckerState = getConstraintManager().removeDeadBindings(CheckerState,
|
|
|
- SymReaper);
|
|
|
-
|
|
|
- assert(StateMgr.haveEqualEnvironments(CheckerState, Pred->getState()) &&
|
|
|
- "Checkers are not allowed to modify the Environment as a part of "
|
|
|
- "checkDeadSymbols processing.");
|
|
|
- assert(StateMgr.haveEqualStores(CheckerState, Pred->getState()) &&
|
|
|
- "Checkers are not allowed to modify the Store as a part of "
|
|
|
- "checkDeadSymbols processing.");
|
|
|
-
|
|
|
- // Create a state based on CleanedState with CheckerState GDM and
|
|
|
- // generate a transition to that state.
|
|
|
- ProgramStateRef CleanedCheckerSt =
|
|
|
+ // Call checkers with the non-cleaned state so that they could query the
|
|
|
+ // values of the soon to be dead symbols.
|
|
|
+ ExplodedNodeSet CheckedSet;
|
|
|
+ getCheckerManager().runCheckersForDeadSymbols(CheckedSet, Pred, SymReaper,
|
|
|
+ DiagnosticStmt, *this, K);
|
|
|
+
|
|
|
+ // For each node in CheckedSet, generate CleanedNodes that have the
|
|
|
+ // environment, the store, and the constraints cleaned up but have the
|
|
|
+ // user-supplied states as the predecessors.
|
|
|
+ StmtNodeBuilder Bldr(CheckedSet, Out, *currBldrCtx);
|
|
|
+ for (const auto I : CheckedSet) {
|
|
|
+ ProgramStateRef CheckerState = I->getState();
|
|
|
+
|
|
|
+ // The constraint manager has not been cleaned up yet, so clean up now.
|
|
|
+ CheckerState =
|
|
|
+ getConstraintManager().removeDeadBindings(CheckerState, SymReaper);
|
|
|
+
|
|
|
+ assert(StateMgr.haveEqualEnvironments(CheckerState, Pred->getState()) &&
|
|
|
+ "Checkers are not allowed to modify the Environment as a part of "
|
|
|
+ "checkDeadSymbols processing.");
|
|
|
+ assert(StateMgr.haveEqualStores(CheckerState, Pred->getState()) &&
|
|
|
+ "Checkers are not allowed to modify the Store as a part of "
|
|
|
+ "checkDeadSymbols processing.");
|
|
|
+
|
|
|
+ // Create a state based on CleanedState with CheckerState GDM and
|
|
|
+ // generate a transition to that state.
|
|
|
+ ProgramStateRef CleanedCheckerSt =
|
|
|
StateMgr.getPersistentStateWithGDM(CleanedState, CheckerState);
|
|
|
- Bldr.generateNode(DiagnosticStmt, I, CleanedCheckerSt, &cleanupTag, K);
|
|
|
- }
|
|
|
+ Bldr.generateNode(DiagnosticStmt, I, CleanedCheckerSt, &cleanupTag, K);
|
|
|
}
|
|
|
}
|
|
|
|