aboutsummaryrefslogtreecommitdiff
path: root/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp')
-rw-r--r--clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp6
1 files changed, 6 insertions, 0 deletions
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index fa11497..d95b332 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -174,6 +174,9 @@ Solver::Result DataflowAnalysisContext::querySolver(
bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
const Formula &F) {
+ if (F.isLiteral(true))
+ return true;
+
// Returns true if and only if truth assignment of the flow condition implies
// 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
@@ -188,6 +191,9 @@ bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
bool DataflowAnalysisContext::flowConditionAllows(Atom Token,
const Formula &F) {
+ if (F.isLiteral(false))
+ return false;
+
llvm::SetVector<const Formula *> Constraints;
Constraints.insert(&arena().makeAtomRef(Token));
Constraints.insert(&F);