The dynamic semantics defined by the Ada Reference Manual impose a set of run-time checks to be generated. By default, the GNAT compiler will insert many run-time checks into the compiled code, including most of those required by the Ada Reference Manual. However, there are two checks that are not enabled in the default mode for efficiency reasons: checks for access before elaboration on subprogram calls, and stack overflow checking (most operating systems do not perform this check by default).
Strict conformance to the Ada Reference Manual can be achieved by adding two compiler options for dynamic checks for access-before-elaboration on subprogram calls and generic instantiations (`-gnatE'), and stack overflow checking (`-fstack-check').
Note that the result of a floating point arithmetic operation in overflow and
invalid situations, when the Machine_Overflows attribute of the result
type is False, is to generate IEEE NaN and infinite values. This is the
case for machines compliant with the IEEE floating-point standard, but on
machines that are not fully compliant with this standard, such as Alpha, the
`-mieee' compiler flag must be used for achieving IEEE confirming
behavior (although at the cost of a significant performance penalty), so
infinite and NaN values are properly generated.