D.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, then the addition may cause overflow since the result is out of range of the type Integer. In this case Constraint_Error will be raised if checks are enabled.

A trickier situation arises in examples like the following:

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

where A is Integer'Last and C is -1. Now 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, then the assignment 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, 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:

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

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 P are both 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 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).