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.
Constraint_Error), or
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).