Commit Graph

4 Commits

Author SHA1 Message Date
Wei Yi Tee 81e6400d8c [clang][dataflow] Return a solution from the solver when `Constraints` are `Satisfiable`.
Differential Revision: https://reviews.llvm.org/D129180
2022-07-07 20:21:19 +00:00
Dmitri Gribenko 63fac424e6 Revert "[clang][dataflow] Return a solution from the solver when `Constraints` are `Satisfiable`."
This reverts commit 19e21887eb. I
accidentally landed the non-final version of the patch that used
decomposition declarations (not yet usable in LLVM/Clang source).
2022-07-07 21:50:52 +02:00
Wei Yi Tee 19e21887eb [clang][dataflow] Return a solution from the solver when `Constraints` are `Satisfiable`.
A truth assignment to atomic boolean values which satisfy `Constraints` will be returned if found by the solver.
This gives us more information which can be helpful for debugging or constructing warning messages.

Reviewed By: hlopko, gribozavr2, sgatev

Differential Revision: https://reviews.llvm.org/D129180
2022-07-07 20:53:47 +02:00
Stanislav Gatev 53dcd9efd1 [clang][dataflow] Add SAT solver interface and implementation
This is part of the implementation of the dataflow analysis framework.
See "[RFC] A dataflow analysis framework for Clang AST" on cfe-dev.

Reviewed-by: ymandel, xazax.hun

Differential Revision: https://reviews.llvm.org/D120289
2022-02-25 14:46:52 +00:00