[PATCH] D153805: Expose DataflowAnalysisContext.querySolver().
Samira Bazuzi via Phabricator via cfe-commits
cfe-commits at lists.llvm.org
Fri Jun 30 08:32:52 PDT 2023
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) {
-------------- next part --------------
A non-text attachment was scrubbed...
Name: D153805.536269.patch
Type: text/x-patch
Size: 1546 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20230630/7e4c81a2/attachment.bin>
More information about the cfe-commits
mailing list