xazax.hun added inline comments.
================
Comment at: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp:79
+ for (BoolValue *Constraint : Env1.getFlowConditionConstraints()) {
+ Expr1 = &Env1.makeAnd(*Expr1, *Constraint);
+ }
----------------
Hmm, interesting.
I think we view every boolean formula at a certain program point implicitly as
`FlowConditionAtThatPoint && Formula`. And the flow condition at a program
point should already be a disjunction of its predecessors.
So it would be interpreted as: `(FlowConditionPred1 || FlowConditionPred2) &&
(FormulaAtPred1 || FormulaAtPred2)`.
While this is great, this is not the strongest condition we could derive.
`(FlowConditionPred1 && FormulaAtPred1) || (FormulaAtPred2 &&
FlowConditionPred2)` created by this code snippet is stronger which is great.
My main concern is whether we would end up seeing an exponential explosion in
the size of these formulas in the number of branches following each other in a
sequence.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D122838/new/
https://reviews.llvm.org/D122838
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
