[analyzer] Indicate if a parent state is infeasible
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: https://github.com/llvm/llvm-project/issues/50883 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: https://github.com/llvm/llvm-project/issues/54272 Differential Revision: https://reviews.llvm.org/D124674
Loading
Please sign in to comment