- condition S * i <> C, assuming that this exit is taken. If
- NO_OVERFLOW is true, then the control variable of the loop does not
- overflow. If NO_OVERFLOW is true or BNDS.below >= 0, then BNDS.up
- contains the upper bound on the value of C. */
+ condition S * i <> C. If NO_OVERFLOW is true, then the control variable of
+ the loop does not overflow. EXIT_MUST_BE_TAKEN is true if we are guaranteed
+ that the loop ends through this exit, i.e., the induction variable ever
+ reaches the value of C.
+
+ The value C is equal to final - base, where final and base are the final and
+ initial value of the actual induction variable in the analysed loop. BNDS
+ bounds the value of this difference when computed in signed type with
+ unbounded range, while the computation of C is performed in an unsigned
+ type with the range matching the range of the type of the induction variable.
+ In particular, BNDS.up contains an upper bound on C in the following cases:
+ -- if the iv must reach its final value without overflow, i.e., if
+ NO_OVERFLOW && EXIT_MUST_BE_TAKEN is true, or
+ -- if final >= base, which we know to hold when BNDS.below >= 0. */