//
// a) IV is either nuw or nsw depending upon signedness (indicated by the
// NoWrap flag).
- // b) loop is single exit with no side effects.
- // c) loop has no abnormal exits
- //
+ // b) the loop is guaranteed to be finite (e.g. is mustprogress and has
+ // no side effects within the loop)
+ // b) loop has a single static exit (with no abnormal exits)
//
// Precondition a) implies that if the stride is negative, this is a single
// trip loop. The backedge taken count formula reduces to zero in this case.