Background (GNAT User’s Guide for Native Platforms)

#### 6.4.1 Background ¶

Overflow checks are checks that the compiler may make to ensure that intermediate results are not out of range. For example:

>     A : Integer;
>     ...
>     A := A + 1;

If `A` has the value `Integer'Last`, the addition will cause overflow since the result is out of range of the type `Integer`. In this case, execution will raise `Constraint_Error` if checks are enabled.

A trickier situation arises in cases like the following:

>     A, C : Integer;
>     ...
>     A := (A + 1) + C;

where `A` is `Integer'Last` and `C` is `-1`. Here, the final result of the expression on the right hand side is `Integer'Last` which is in range, but the question arises whether the intermediate addition of `(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.

- raise an exception (`Constraint_Error`), or
- yield the correct mathematical result which is then used in subsequent operations.

If the compiler chooses the first approach, the execution of this example will indeed raise `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, it can perform both additions yielding the correct mathematical result, which is in range, so no exception is 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 you port programs. Most typically, this arises in a situation where the original compiler did not raise an exception and you move the application 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:

>     procedure P (A, B : Integer) with
>       Pre => A + B <= Integer'Last;

We often want to regard arithmetic in a context such as this from a purely mathematical point of view. So, for example, if the two actual parameters for a call to `P` are both `Integer'Last` then the precondition should be evaluated as `False`. If we’re 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 `Assert_Error`) or causes an intermediate overflow (raising `Constraint_Error`) up to the implementation.

The situation is worse in a case such as the following:

>     procedure Q (A, B, C : Integer) with
>       Pre => A + B + C <= Integer'Last;

Consider the call

>     Q (A => Integer'Last, B => 1, C => -1);

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