Management of Overflows in GNAT (GNAT User’s Guide for Native Platforms)

#### 6.4.2 Management of Overflows in GNAT ¶

To deal with the portability issue and with the problem of mathematical versus run-time interpretation of the expressions in assertions, GNAT provides comprehensive control over the handling of intermediate overflows. It can operate in three modes, and in addition, permits separate selection of operating modes for the expressions within assertions (here the term ‘assertions’ is used in the technical sense, which includes preconditions and so forth) and for expressions appearing outside assertions.

The three modes are:

- ‘Use base type for intermediate operations’ (`STRICT`)

  In this mode, all intermediate results for predefined arithmetic operators are computed using the base type, and the result must be in range of the base type. If this is not the case, then either an exception is raised (if overflow checks are enabled) or the execution is erroneous (if overflow checks are suppressed). This is the normal default mode.

- ‘Most intermediate overflows avoided’ (`MINIMIZED`)

  In this mode, the compiler attempts to avoid intermediate overflows by using a larger integer type, typically `Long_Long_Integer`, as the type in which arithmetic is performed for predefined arithmetic operators. This may be slightly more expensive at run time (compared to suppressing intermediate overflow checks), though the cost is negligible on modern 64-bit machines. For the examples given earlier, no intermediate overflows would have resulted in exceptions, since the intermediate results are all in the range of `Long_Long_Integer` (typically 64-bits on nearly all implementations of GNAT). In addition, if checks are enabled, this reduces the number of checks that must be made, so this choice may actually result in an improvement in space and time behavior.

  However, there are cases where `Long_Long_Integer` is not large enough. Consider the following example:

  >     procedure R (A, B, C, D : Integer) with
  >       Pre => (A**2 * B**2) / (C**2 * D**2) <= 10;

  where `A` = `B` = `C` = `D` = `Integer'Last`. Now the intermediate results are out of the range of `Long_Long_Integer` even though the final result is in range and the precondition is `True` from a mathematical point of view. In such a case, operating in this mode, an overflow occurs for the intermediate computation (which is why this mode says ‘most’ intermediate overflows are avoided). In this case, an exception is raised if overflow checks are enabled, and the execution is erroneous if overflow checks are suppressed.

- ‘All intermediate overflows avoided’ (`ELIMINATED`)

  In this mode, the compiler avoids all intermediate overflows by using arbitrary precision arithmetic as required. In this mode, the above example with `A**2 * B**2` would not cause intermediate overflow, because the intermediate result would be evaluated using sufficient precision, and the result of evaluating the precondition would be `True`.

  This mode has the advantage of avoiding any intermediate overflows, but at the expense of significant run-time overhead, including the use of a library (included automatically in this mode) for multiple-precision arithmetic.

  This mode provides cleaner semantics for assertions, since now the run-time behavior emulates true arithmetic behavior for the predefined arithmetic operators, meaning that there is never a conflict between the mathematical view of the assertion and its run-time behavior.

  Note that in this mode, the behavior is unaffected by whether or not overflow checks are suppressed, since overflow does not occur. Gigantic intermediate expressions can still raise `Storage_Error` as a result of attempting to compute the results of such expressions (e.g. `Integer'Last ** Integer'Last`) but overflow is impossible.

Note that these modes apply only to the evaluation of predefined arithmetic, membership, and comparison operators for signed integer arithmetic.

For fixed-point arithmetic, you suppress checks. But if checks are enabled, fixed-point values are always checked for overflow against the base type for intermediate expressions (i.e., such checks always operate in the equivalent of `STRICT` mode).

For floating-point, on nearly all architectures, `Machine_Overflows` is `False`, and IEEE infinities are generated, so overflow exceptions are never raised. If you want to avoid infinities and check that final results of expressions are in range, you can declare a constrained floating-point type and range checks are carried out in the normal manner (with infinite values always failing all range checks).