@@ -3749,9 +3749,10 @@ ExprEngine::getEagerlyAssumeBifurcationTags() {
37493749 return std::make_pair (&TrueTag, &FalseTag);
37503750}
37513751
3752- // / The last expression where EagerlyAssume produced two transitions (i.e. it
3753- // / activated and the true and false cases were both feasible).
3754- REGISTER_TRAIT_WITH_PROGRAMSTATE (LastEagerlyAssumeBifurcationAt, const Expr *)
3752+ // / If the last EagerlyAssume attempt was successful (i.e. the true and false
3753+ // / cases were both feasible), this state trait stores the expression where it
3754+ // / happened; otherwise this holds nullptr.
3755+ REGISTER_TRAIT_WITH_PROGRAMSTATE (LastEagerlyAssumeExprIfSuccessful, const Expr *)
37553756
37563757void ExprEngine::evalEagerlyAssumeBifurcation(ExplodedNodeSet &Dst,
37573758 ExplodedNodeSet &Src,
@@ -3768,6 +3769,7 @@ void ExprEngine::evalEagerlyAssumeBifurcation(ExplodedNodeSet &Dst,
37683769 }
37693770
37703771 ProgramStateRef State = Pred->getState ();
3772+ State = State->set <LastEagerlyAssumeExprIfSuccessful>(nullptr );
37713773 SVal V = State->getSVal (Ex, Pred->getLocationContext ());
37723774 std::optional<nonloc::SymbolVal> SEV = V.getAs <nonloc::SymbolVal>();
37733775 if (SEV && SEV->isExpression ()) {
@@ -3776,8 +3778,8 @@ void ExprEngine::evalEagerlyAssumeBifurcation(ExplodedNodeSet &Dst,
37763778 auto [StateTrue, StateFalse] = State->assume (*SEV);
37773779
37783780 if (StateTrue && StateFalse) {
3779- StateTrue = StateTrue->set <LastEagerlyAssumeBifurcationAt >(Ex);
3780- StateFalse = StateFalse->set <LastEagerlyAssumeBifurcationAt >(Ex);
3781+ StateTrue = StateTrue->set <LastEagerlyAssumeExprIfSuccessful >(Ex);
3782+ StateFalse = StateFalse->set <LastEagerlyAssumeExprIfSuccessful >(Ex);
37813783 }
37823784
37833785 // First assume that the condition is true.
@@ -3799,7 +3801,7 @@ void ExprEngine::evalEagerlyAssumeBifurcation(ExplodedNodeSet &Dst,
37993801
38003802bool ExprEngine::didEagerlyAssumeBifurcateAt (ProgramStateRef State,
38013803 const Expr *Ex) const {
3802- return Ex && State->get <LastEagerlyAssumeBifurcationAt >() == Ex;
3804+ return Ex && State->get <LastEagerlyAssumeExprIfSuccessful >() == Ex;
38033805}
38043806
38053807void ExprEngine::VisitGCCAsmStmt (const GCCAsmStmt *A, ExplodedNode *Pred,
0 commit comments