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) {
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) {
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
