D.2 Overflow Checking Modes in GNAT

To deal with the portability issue, and with the problem of mathematical versus run-time intepretation of the expressions in assertions, GNAT provides comprehensive control over the handling of intermediate overflow. GNAT can operate in three modes, and furthemore, 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. It is possible for gigantic intermediate expressions to 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 aritmetic.

For fixed-point arithmetic, checks can be suppressed. But if checks are enabled then fixed-point values are always checked for overflow against the base type for intermediate expressions (that is 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, then you can declare a constrained floating-point type, and range checks will be carried out in the normal manner (with infinite values always failing all range checks).