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 three checks that are not enabled in the default mode for efficiency reasons: arithmetic overflow checking for integer operations (including division by zero), 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 three compiler options for overflow checking for integer operations (`-gnato'), 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.