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:
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.
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.
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).