================
@@ -3776,6 +3829,11 @@ void
ExprEngine::evalEagerlyAssumeBinOpBifurcation(ExplodedNodeSet &Dst,
ProgramStateRef StateTrue, StateFalse;
std::tie(StateTrue, StateFalse) = state->assume(*SEV);
+ if (StateTrue && StateFalse) {
+ StateTrue = StateTrue->set<LastEagerlyAssumeAssumptionAt>(Ex);
+ StateFalse = StateFalse->set<LastEagerlyAssumeAssumptionAt>(Ex);
+ }
----------------
NagyDonat wrote:
This is recorded here because this is where I clearly see that `EagerlyAssume`
splits the state.
Later, where `processBranch` calls `assumeCondition`, we are already on one of
these two separate branches, and we'd need to search within the earlier
`ExplodedNode`s to find the state split caused by `EagerlyAssume`. I strongly
suspect that this might involve the traversal of several nodes (e.g. if some
checker callback or rare C++ lifetime magic activates) and I think that a
solution like this would be too slow and fragile.
Also I don't really believe that "polluting states" is a serious issue, because
I strongly suspect that merging states and joining execution paths only happens
in very specific trivial circumstances. (Also note that when we search
backwards on the execution path, we usually follow the first predecessor,
discounting the possibility of having more than one predecessor.)
https://github.com/llvm/llvm-project/pull/109804
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
