Author: Samira Bazuzi Date: 2023-07-01T00:15:45+02:00 New Revision: 3b29b8a2aba205b59163ba11c537fbfe25133181
URL: https://github.com/llvm/llvm-project/commit/3b29b8a2aba205b59163ba11c537fbfe25133181 DIFF: https://github.com/llvm/llvm-project/commit/3b29b8a2aba205b59163ba11c537fbfe25133181.diff LOG: Expose DataflowAnalysisContext.querySolver(). This allows for use of the same solver used by the DAC for additional solving post-analysis and thus shared use of MaxIterations in WatchedLiteralsSolver. Reviewed By: ymandel, gribozavr2, sammccall Differential Revision: https://reviews.llvm.org/D153805 Added: Modified: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h Removed: ################################################################################ diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h index eba42fc3418f68..735f2b2d85021c 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -175,6 +175,14 @@ class DataflowAnalysisContext { 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 @@ class DataflowAnalysisContext { 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