NagyDonat wrote:
> When asked some AI to confirm that this is NFC, it told me that there might
> be an issue:
>
> > Previously, when both `StateTrue` and `StateFalse` were `null` (the
> > symbolic condition is unsatisfiable in the current state), `Pred` remained
> > in the Frontier/Dst because `NodeBuilder::generateNode` was never called
> > and could never erase it. With this patch, that path is dropped: no
> > `Dst.insert(Pred)` runs.
>
> I'm not sure, but AFAIK `StateTrue` and `StateFalse` could be null at the
> same time, so this sounds plausible to me.
Actually, `StateTrue` and `StateFalse` cannot be both null at the same time,
because this the corner case when `ConstraintManager::assumeDualImpl`
introduces PosteriorlyOverconstrained states instead of returning `{nullptr,
nullptr}`. Therefore my conversion happens to be NFC.
(By the way, this was a helpful review comment, because I didn't think about
this corner case. Without the PosteriorlyOverconstrained hack the old code
would be logically incorrect – in that one very rare case – and the new would
be the logically correct transition.)
https://github.com/llvm/llvm-project/pull/204371
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
