+@c **********************************
+@node Overflow Check Handling in GNAT
+@appendix Overflow Check Handling in GNAT
+@cindex Overflow checks
+@cindex Checks (overflow)
+@c **********************************
+
+@menu
+* Background::
+* Overflow Checking Modes in GNAT::
+* Specifying the Desired Mode::
+* Default Settings::
+* Implementation Notes::
+@end menu
+
+
+@node Background
+@section Background
+
+@noindent
+Overflow checks are checks that the compiler may make to ensure
+that intermediate results are not out of range. For example:
+
+@smallexample @c ada
+ A : Integer;
+ ...
+ A := A + 1;
+@end smallexample
+
+@noindent
+if @code{A} has the value @code{Integer'Last}, then the addition may cause
+overflow since the result is out of range of the type @code{Integer}.
+In this case @code{Constraint_Error} will be raised if checks are
+enabled.
+
+A trickier situation arises in examples like the following:
+
+@smallexample @c ada
+ A, C : Integer;
+ ...
+ A := (A + 1) + C;
+@end smallexample
+
+@noindent
+where @code{A} is @code{Integer'Last} and @code{C} is @code{-1}.
+Now the final result of the expression on the right hand side is
+@code{Integer'Last} which is in range, but the question arises whether the
+intermediate addition of @code{(A + 1)} raises an overflow error.
+
+The (perhaps surprising) answer is that the Ada language
+definition does not answer this question. Instead it leaves
+it up to the implementation to do one of two things if overflow
+checks are enabled.
+
+@itemize @bullet
+@item
+raise an exception (@code{Constraint_Error}), or
+
+@item
+yield the correct mathematical result which is then used in
+subsequent operations.
+@end itemize
+
+@noindent
+If the compiler chooses the first approach, then the assignment of this
+example will indeed raise @code{Constraint_Error} if overflow checking is
+enabled, or result in erroneous execution if overflow checks are suppressed.
+
+But if the compiler
+chooses the second approach, then it can perform both additions yielding
+the correct mathematical result, which is in range, so no exception
+will be raised, and the right result is obtained, regardless of whether
+overflow checks are suppressed.
+
+Note that in the first example an
+exception will be raised in either case, since if the compiler
+gives the correct mathematical result for the addition, it will
+be out of range of the target type of the assignment, and thus
+fails the range check.
+
+This lack of specified behavior in the handling of overflow for
+intermediate results is a source of non-portability, and can thus
+be problematic when programs are ported. Most typically this arises
+in a situation where the original compiler did not raise an exception,
+and then the application is moved to a compiler where the check is
+performed on the intermediate result and an unexpected exception is
+raised.
+
+Furthermore, when using Ada 2012's preconditions and other
+assertion forms, another issue arises. Consider:
+
+@smallexample @c ada
+ procedure P (A, B : Integer) with
+ Pre => A + B <= Integer'Last;
+@end smallexample
+
+@noindent
+One often wants to regard arithmetic in a context like this from
+a mathematical point of view. So for example, if the two actual parameters
+for a call to @code{P} are both @code{Integer'Last}, then
+the precondition should be regarded as False. If we are executing
+in a mode with run-time checks enabled for preconditions, then we would
+like this precondition to fail, rather than raising an exception
+because of the intermediate overflow.
+
+However, the language definition leaves the specification of
+whether the above condition fails (raising @code{Assert_Error}) or
+causes an intermediate overflow (raising @code{Constraint_Error})
+up to the implementation.
+
+The situation is worse in a case such as the following:
+
+@smallexample @c ada
+ procedure Q (A, B, C : Integer) with
+ Pre => A + B + C <= Integer'Last;
+@end smallexample
+
+@noindent
+Consider the call
+
+@smallexample @c ada
+ Q (A => Integer'Last, B => 1, C => -1);
+@end smallexample
+
+@noindent
+From a mathematical point of view the precondition
+is True, but at run time we may (but are not guaranteed to) get an
+exception raised because of the intermediate overflow (and we really
+would prefer this precondition to be considered True at run time).
+
+@node Overflow Checking Modes in GNAT
+@section Overflow Checking Modes in GNAT
+
+@noindent
+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:
+
+@itemize @bullet
+@item @i{Use base type for intermediate operations} (@code{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.
+
+@item @i{Most intermediate overflows avoided} (@code{MINIMIZED})
+
+ In this mode, the compiler attempts to avoid intermediate overflows by
+ using a larger integer type, typically @code{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
+ @code{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 @code{Long_Long_Integer} is not large
+ enough, consider the following example:
+
+@smallexample @c ada
+ procedure R (A, B, C, D : Integer) with
+ Pre => (A**2 * B**2) / (C**2 * D**2) <= 10;
+@end smallexample
+
+ where @code{A} = @code{B} = @code{C} = @code{D} = @code{Integer'Last}.
+ Now the intermediate results are
+ out of the range of @code{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 @i{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.
+
+@item @i{All intermediate overflows avoided} (@code{ELIMINATED})
+
+ In this mode, the compiler avoids all intermediate overflows
+ by using arbitrary precision arithmetic as required. In this
+ mode, the above example with @code{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
+ @code{Storage_Error} as a result of attempting to compute the
+ results of such expressions (e.g. @code{Integer'Last ** Integer'Last})
+ but overflow is impossible.
+
+
+@end itemize
+
+@noindent
+ 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 @code{STRICT} mode).
+
+ For floating-point, on nearly all architectures, @code{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).
+
+
+@c -------------------------
+@node Specifying the Desired Mode
+@section Specifying the Desired Mode
+
+@noindent
+The desired mode of for handling intermediate overflow can be specified using
+either the @code{Overflow_Mode} pragma or an equivalent compiler switch.
+The pragma has the form
+@cindex pragma @code{Overflow_Mode}
+
+@smallexample @c ada
+ pragma Overflow_Mode ([General =>] MODE [, [Assertions =>] MODE]);
+@end smallexample
+
+@noindent
+where @code{MODE} is one of
+
+@itemize @bullet
+@item @code{STRICT}: intermediate overflows checked (using base type)
+@item @code{MINIMIZED}: minimize intermediate overflows
+@item @code{ELIMINATED}: eliminate intermediate overflows
+@end itemize
+
+@noindent
+The case is ignored, so @code{MINIMIZED}, @code{Minimized} and
+@code{minimized} all have the same effect.
+
+If only the @code{General} parameter is present, then the given @code{MODE}
+applies
+to expressions both within and outside assertions. If both arguments
+are present, then @code{General} applies to expressions outside assertions,
+and @code{Assertions} applies to expressions within assertions. For example:
+
+@smallexample @c ada
+ pragma Overflow_Mode
+ (General => Minimized, Assertions => Eliminated);
+@end smallexample
+
+@noindent
+specifies that general expressions outside assertions be evaluated
+in ``minimize intermediate overflows'' mode, and expressions within
+assertions be evaluated in ``eliminate intermediate overflows'' mode.
+This is often a reasonable choice, avoiding excessive overhead
+outside assertions, but assuring a high degree of portability
+when importing code from another compiler, while incurring
+the extra overhead for assertion expressions to ensure that
+the behavior at run time matches the expected mathematical
+behavior.
+
+The @code{Overflow_Mode} pragma has the same scoping and placement
+rules as pragma @code{Suppress}, so it can occur either as a
+configuration pragma, specifying a default for the whole
+program, or in a declarative scope, where it applies to the
+remaining declarations and statements in that scope.
+
+Note that pragma @code{Overflow_Mode} does not affect whether
+overflow checks are enabled or suppressed. It only controls the
+method used to compute intermediate values. To control whether
+overflow checking is enabled or suppressed, use pragma @code{Suppress}
+or @code{Unsuppress} in the usual manner
+
+Additionally, a compiler switch @option{-gnato?} or @option{-gnato??}
+can be used to control the checking mode default (which can be subsequently
+overridden using pragmas).
+@cindex @option{-gnato?} (gcc)
+@cindex @option{-gnato??} (gcc)
+
+Here `@code{?}' is one of the digits `@code{1}' through `@code{3}':
+
+@itemize @bullet
+@item @code{1}:
+use base type for intermediate operations (@code{STRICT})
+@item @code{2}:
+minimize intermediate overflows (@code{MINIMIZED})
+@item @code{3}:
+eliminate intermediate overflows (@code{ELIMINATED})
+@end itemize
+
+@noindent
+As with the pragma, if only one digit appears then it applies to all
+cases; if two digits are given, then the first applies outside
+assertions, and the second within assertions. Thus the equivalent
+of the example pragma above would be @option{-gnato23}.
+
+If no digits follow the @option{-gnato}, then it is equivalent to
+@option{-gnato11},
+causing all intermediate operations to be computed using the base
+type (@code{STRICT} mode).
+
+In addition to setting the mode used for computation of intermediate
+results, the @code{-gnato} switch also enables overflow checking (which
+is suppressed by default). It thus combines the effect of using
+a pragma @code{Overflow_Mode} and pragma @code{Unsuppress}.
+
+
+@c -------------------------
+@node Default Settings
+@section Default Settings
+
+The default mode for overflow checks is
+
+@smallexample
+ General => Strict
+@end smallexample
+
+@noindent
+which causes all computations both inside and outside assertions to use
+the base type. In addition overflow checks are suppressed.
+
+This retains compatibility with previous versions of
+GNAT which suppressed overflow checks by default and always
+used the base type for computation of intermediate results.
+
+The switch @option{-gnato} (with no digits following) is equivalent to
+@cindex @option{-gnato} (gcc)
+
+@smallexample
+ General => Strict
+@end smallexample
+
+@noindent
+which causes overflow checking of all intermediate overflows
+both inside and outside assertions against the base type.
+This provides compatibility
+with this switch as implemented in previous versions of GNAT.
+
+The pragma @code{Suppress (Overflow_Check)} disables overflow
+checking, but it has no effect on the method used for computing
+intermediate results.
+
+The pragma @code{Unsuppress (Overflow_Check)} enables overflow
+checking, but it has no effect on the method used for computing
+intermediate results.
+
+@c -------------------------
+@node Implementation Notes
+@section Implementation Notes
+
+In practice on typical 64-bit machines, the @code{MINIMIZED} mode is
+reasonably efficient, and can be generally used. It also helps
+to ensure compatibility with code imported from some other
+compiler to GNAT.
+
+Setting all intermediate overflows checking (@code{CHECKED} mode)
+makes sense if you want to
+make sure that your code is compatible with any other possible
+Ada implementation. This may be useful in ensuring portability
+for code that is to be exported to some other compiler than GNAT.
+
+
+The Ada standard allows the reassociation of expressions at
+the same precedence level if no parentheses are present. For
+example, @w{@code{A+B+C}} parses as though it were @w{@code{(A+B)+C}}, but
+the compiler can reintepret this as @w{@code{A+(B+C)}}, possibly
+introducing or eliminating an overflow exception. The GNAT
+compiler never takes advantage of this freedom, and the
+expression @w{@code{A+B+C}} will be evaluated as @w{@code{(A+B)+C}}.
+If you need the other order, you can write the parentheses
+explicitly @w{@code{A+(B+C)}} and GNAT will respect this order.
+
+The use of @code{ELIMINATED} mode will cause the compiler to
+automatically include an appropriate arbitrary precision
+integer arithmetic package. The compiler will make calls
+to this package, though only in cases where it cannot be
+sure that @code{Long_Long_Integer} is sufficient to guard against
+intermediate overflows. This package does not use dynamic
+alllocation, but it does use the secondary stack, so an
+appropriate secondary stack package must be present (this
+is always true for standard full Ada, but may require
+specific steps for restricted run times such as ZFP).
+
+Although @code{ELIMINATED} mode causes expressions to use arbitrary
+precision arithmetic, avoiding overflow, the final result
+must be in an appropriate range. This is true even if the
+final result is of type @code{[Long_[Long_]]Integer'Base}, which
+still has the same bounds as its associated constrained
+type at run-time.
+
+Currently, the @code{ELIMINATED} mode is only available on target
+platforms for which @code{Long_Long_Integer} is 64-bits (nearly all GNAT
+platforms).