[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