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 semmle.code.cpp.controlflow.internal.ConstantExprspredicate loopConditionAlwaysTrueUponEntry(ControlFlowNode loop, Expr condition)