9.7 Dynamic Elaboration Model in GNAT

The dynamic model assumes that all code within all units in a partition is elaboration code. As a result, run-time checks are installed for each scenario regardless of whether the target is internal or external. The checks can be suppressed using pragma Suppress (Elaboration_Check). This behavior is identical to that specified by the Ada Reference Manual. The following example showcases run-time checks installed by GNAT to verify the elaboration state of package Dynamic_Model.

with Server;
package body Dynamic_Model is
   procedure API is
   begin
      ...
   end API;

   <check that the body of Server.Gen is elaborated>
   package Inst is new Server.Gen;

   T : Server.Task_Type;

begin
   <check that the body of Server.Task_Type is elaborated>

   <check that the body of Server.Proc is elaborated>
   Server.Proc;
end Dynamic_Model;

The checks verify that the body of a target has been successfully elaborated before a scenario activates, calls, or instantiates a target.

Note that no scenario within package Dynamic_Model calls procedure API. In fact, procedure API may not be invoked by elaboration code within the partition, however the dynamic model assumes that this can happen.

The dynamic model emits very few diagnostics, but can make suggestions on missing Elaborate and Elaborate_All pragmas for library-level scenarios. This information is available when compiler switch -gnatel is in effect.

1. with Server;
2. package body Dynamic_Model is
3.    Val : constant Integer := Server.Func;
                                      |
   >>> info: call to "Func" during elaboration
   >>> info: missing pragma "Elaborate_All" for unit "Server"

4. end Dynamic_Model;