[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