[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.

Related bug:
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...
Name: D124674.426061.patch
Type: text/x-patch
Size: 7252 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20220429/91308f55/attachment.bin>

More information about the cfe-commits mailing list