[PATCH] D129180: [clang][dataflow] Return a solution from the solver when `Constraints` are `Satisfiable`.
Stanislav Gatev via Phabricator via cfe-commits
cfe-commits at lists.llvm.org
Thu Jul 7 03:00:37 PDT 2022
sgatev accepted this revision.
sgatev added inline comments.
================
Comment at: clang/include/clang/Analysis/FlowSensitive/Solver.h:78
+ Status Status;
+ std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution;
};
----------------
`#include "llvm/ADT/DenseMap.h"`
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:200
if (!SubValsToVar.try_emplace(Val, NextVar).second)
continue;
----------------
Let's create a local `Var` variable initialized to `NextVar` and use that here and below, where `NextVar - 1` is currently used.
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:471-472
private:
+ // Returns a satisfying truth assignment to the atomic values in the boolean
+ // formula.
+ llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
----------------
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D129180/new/
https://reviews.llvm.org/D129180
More information about the cfe-commits
mailing list