Member predicate LoopEntryConditionEvaluator::ignoreNonAnalyzableVariableDefinition
When evaluating a syntactic subexpression of loop condition e
,
we may ignore non-analyzable variable definition def
for
variable v
, provided that def
is in the body of the loop and
cannot reach the loop entry point.
Example:
done = false;
while (!done) {
f(&done); // can be ignored
}
while (...) {
done = false;
while (!done) {
f(&done); // can be ignored
}
}
done = false;
while (...) {
while (!done) {
f(&done); // cannot be ignored
}
}
predicate ignoreNonAnalyzableVariableDefinition(Expr e, Variable v, StmtParent def)