bazuzi updated this revision to Diff 536269.
bazuzi added a comment.
Updated function comment to remove unnecessary repetition and include
newly-discovered caveat re: flow conditions.
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
@@ -174,6 +174,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::DenseSet<BoolValue *> Constraints);
+
private:
friend class Environment;
@@ -203,13 +211,6 @@
AtomicBoolValue &Token, llvm::DenseSet<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::DenseSet<BoolValue *> Constraints);
-
/// Returns true if the solver is able to prove that there is no satisfying
/// assignment for `Constraints`
bool isUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) {
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -174,6 +174,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::DenseSet<BoolValue *> Constraints);
+
private:
friend class Environment;
@@ -203,13 +211,6 @@
AtomicBoolValue &Token, llvm::DenseSet<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::DenseSet<BoolValue *> Constraints);
-
/// Returns true if the solver is able to prove that there is no satisfying
/// assignment for `Constraints`
bool isUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) {
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
