[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().

Dmitri Gribenko via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Fri Jun 30 15:15:55 PDT 2023


This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rG3b29b8a2aba2: Expose DataflowAnalysisContext.querySolver(). (authored by bazuzi, committed by gribozavr).

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D153805/new/

https://reviews.llvm.org/D153805

Files:
  clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h


Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -175,6 +175,14 @@
 
   Arena &arena() { return *A; }
 
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  ///
+  /// Flow conditions are not incorporated, so they may need to be manually
+  /// included in `Constraints` to provide contextually-accurate results, e.g.
+  /// if any definitions or relationships of the values in `Constraints` have
+  /// been stored in flow conditions.
+  Solver::Result querySolver(llvm::SetVector<BoolValue *> Constraints);
+
 private:
   friend class Environment;
 
@@ -204,13 +212,6 @@
       AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
       llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
 
-  /// Returns the outcome of satisfiability checking on `Constraints`.
-  /// Possible outcomes are:
-  /// - `Satisfiable`: A satisfying assignment exists and is returned.
-  /// - `Unsatisfiable`: A satisfying assignment does not exist.
-  /// - `TimedOut`: The search for a satisfying assignment was not completed.
-  Solver::Result querySolver(llvm::SetVector<BoolValue *> Constraints);
-
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::SetVector<BoolValue *> Constraints) {


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D153805.536454.patch
Type: text/x-patch
Size: 1550 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20230630/dffc6fe9/attachment.bin>


More information about the cfe-commits mailing list