In addition to Ada semantics and rules synthesized from them, GNAT offers three elaboration models to aid the programmer with specifying the correct elaboration order and to diagnose elaboration problems.
This is the most permissive of the three elaboration models and emulates the behavior specified by the Ada Reference Manual. When the dynamic model is in effect, GNAT makes the following assumptions:
GNAT performs extensive diagnostics on a unit-by-unit basis for all scenarios that invoke internal targets. In addition, GNAT generates run-time checks for all external targets and for all scenarios that may exhibit ABE problems.
The elaboration order is obtained by honoring all `with' clauses, purity and preelaborability of units, and elaboration-control pragmas. The dynamic model attempts to take all invocations in elaboration code into account. If an invocation leads to a circularity, GNAT ignores the invocation based on the assumptions stated above. An order obtained using the dynamic model may fail an ABE check at run time when GNAT ignored an invocation.
The dynamic model is enabled with compiler switch -gnatE
.
This is the middle ground of the three models. When the static model is in effect, GNAT makes the following assumptions:
GNAT performs extensive diagnostics on a unit-by-unit basis for all scenarios that invoke internal targets. In addition, GNAT generates run-time checks for all external targets and for all scenarios that may exhibit ABE problems.
The elaboration order is obtained by honoring all `with' clauses, purity and preelaborability of units, presence of elaboration-control pragmas, and all invocations in elaboration code. An order obtained using the static model is guaranteed to be ABE problem-free, excluding dispatching calls and access-to-subprogram types.
The static model is the default model in GNAT.
This is the most conservative of the three models and enforces the SPARK
rules of elaboration as defined in the SPARK Reference Manual, section 7.7.
The SPARK model is in effect only when a scenario and a target reside in a
region subject to SPARK_Mode On
, otherwise the dynamic or static model
is in effect.
The SPARK model is enabled with compiler switch -gnatd.v
.
In addition to the three elaboration models outlined above, GNAT provides the following legacy models:
-gnatH
.
-H
.
The dynamic, legacy, and static models can be relaxed using compiler switch
-gnatJ
, making them more permissive. Note that in this mode, GNAT
may not diagnose certain elaboration issues or install run-time checks.