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