2 files changed, 21 insertions, 8 deletions
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 6a1feb2..40de6cd 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -145,19 +145,28 @@ Solver::Result DataflowAnalysisContext::querySolver(
 }
 
 bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
-                                                   const Formula &Val) {
+                                                   const Formula &F) {
   // Returns true if and only if truth assignment of the flow condition implies
-  // that `Val` is also true. We prove whether or not this property holds by
+  // that `F` is also true. We prove whether or not this property holds by
   // reducing the problem to satisfiability checking. In other words, we attempt
-  // to show that assuming `Val` is false makes the constraints induced by the
+  // to show that assuming `F` is false makes the constraints induced by the
   // flow condition unsatisfiable.
   llvm::SetVector<const Formula *> Constraints;
   Constraints.insert(&arena().makeAtomRef(Token));
-  Constraints.insert(&arena().makeNot(Val));
+  Constraints.insert(&arena().makeNot(F));
   addTransitiveFlowConditionConstraints(Token, Constraints);
   return isUnsatisfiable(std::move(Constraints));
 }
 
+bool DataflowAnalysisContext::flowConditionAllows(Atom Token,
+                                                  const Formula &F) {
+  llvm::SetVector<const Formula *> Constraints;
+  Constraints.insert(&arena().makeAtomRef(Token));
+  Constraints.insert(&F);
+  addTransitiveFlowConditionConstraints(Token, Constraints);
+  return isSatisfiable(std::move(Constraints));
+}
+
 bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1,
                                                  const Formula &Val2) {
   llvm::SetVector<const Formula *> Constraints;
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index 00e56ce..cf1e9eb 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -929,12 +929,16 @@ StorageLocation &Environment::createObjectInternal(const ValueDecl *D,
   return Loc;
 }
 
-void Environment::addToFlowCondition(const Formula &Val) {
-  DACtx->addFlowConditionConstraint(FlowConditionToken, Val);
+void Environment::assume(const Formula &F) {
+  DACtx->addFlowConditionConstraint(FlowConditionToken, F);
 }
 
-bool Environment::flowConditionImplies(const Formula &Val) const {
-  return DACtx->flowConditionImplies(FlowConditionToken, Val);
+bool Environment::proves(const Formula &F) const {
+  return DACtx->flowConditionImplies(FlowConditionToken, F);
+}
+
+bool Environment::allows(const Formula &F) const {
+  return DACtx->flowConditionAllows(FlowConditionToken, F);
 }
 
 void Environment::dump(raw_ostream &OS) const {