[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible
Gabor Marton via Phabricator via cfe-commits
cfe-commits at lists.llvm.org
Fri Apr 29 08:15:53 PDT 2022
martong created this revision.
martong added reviewers: NoQ, steakhal, ASDenysPetrov, Szelethus, xazax.hun.
Herald added subscribers: manas, gamesh411, dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware.
Herald added a project: All.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
In some cases a parent State is already infeasible, but we recognize
this only if an additonal constraint is added. This patch is the first
of a series to address this issue. In this patch `assumeDual` is changed
to clone the parent State but with an `Infeasible` flag set, and this
infeasible-parent is returned both for the true and false case. Then
when we add a new transition in the exploded graph and the destination
is marked as infeasible, the node will be a sink node.
Actually, this patch does not solve that bug in the solver, rather with
this patch we can handle the general parent-infeasible cases.
Next step would be to change the State API and require all checkers to
use the `assume*Dual` API and deprecate the simple `assume` calls.
Hopefully, the next patch will introduce `assumeInBoundDual` and will
solve the CRASH we have here:
rG LLVM Github Monorepo
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 7252 bytes
Desc: not available
More information about the cfe-commits