Member predicate ConstantExprs::ForLoopEntryConditionEvaluator::ignoreVariableAssignment
When evaluating a syntactic subexpression of loop condition e
,
we may ignore the expression value
assigned to variable v
,
provided that value
is in the body of the loop and cannot reach
the loop entry point.
Example:
done = false;
while (!done) {
done = true; // can be ignored
}
while (...) {
done = false;
while (!done) {
done = true; // can be ignored
}
}
done = false;
while (...) {
while (!done) {
done = true; // cannot be ignored
}
}
predicate ignoreVariableAssignment(Expr e, Variable v, Expr value)