[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
Wed Jul 6 05:46:41 PDT 2022
sgatev added inline comments.
================
Comment at: clang/include/clang/Analysis/FlowSensitive/Solver.h:45
+ enum class Assignment : int8_t {
+ Unassigned = -1,
+ AssignedFalse = 0,
----------------
A solution consists of true/false assignments for all variables. Having an `Unassigned` option seems confusing. I suggest defining only two values in this enum and translating `WatchedLiteralsSolver`'s internal representation to `Solution` right before returning it, in `buildValAssignment`.
================
Comment at: clang/include/clang/Analysis/FlowSensitive/Solver.h:50-57
+ static Result Unsatisfiable() { return Result(Status::Unsatisfiable, {}); }
+
+ static Result TimedOut() { return Result(Status::TimedOut, {}); }
+
+ static Result
+ Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) {
+ return Result(Status::Satisfiable, std::move(Solution));
----------------
Let's document these members.
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