Predicate loopConditionAlwaysTrueUponEntry

The condition condition for the loop loop is provably true upon entry. That is, at least one iteration of the loop is guaranteed.

Import path

import cpp

predicate loopConditionAlwaysTrueUponEntry(ControlFlowNode loop, Expr condition)