bazuzi created this revision.
bazuzi added reviewers: ymandel, gribozavr2, xazax.hun.
Herald added a reviewer: NoQ.
Herald added a project: All.
bazuzi requested review of this revision.
Herald added a project: clang.
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.
Repository:
rG LLVM Github Monorepo
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,13 @@
Arena &arena() { return *A; }
+ /// 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);
+
private:
friend class Environment;
@@ -203,13 +210,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,13 @@
Arena &arena() { return *A; }
+ /// 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);
+
private:
friend class Environment;
@@ -203,13 +210,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
