9.8 Static Elaboration Model in GNAT

In contrast to the dynamic model, the static model is more precise in its analysis of elaboration code. The model makes a clear distinction between internal and external targets, and resorts to different diagnostics and run-time checks based on the nature of the target.

• * `Internal targets'

  The static model performs extensive diagnostics on scenarios which elaborate or execute internal targets. The warnings resulting from these diagnostics are enabled by default, but can be suppressed selectively with pragma Warnings (Off) or globally with compiler switch -gnatwL.

   1. package body Static_Model is
   2.    generic
   3.       with function Func return Integer;
   4.    package Gen is
   5.       Val : constant Integer := Func;
   6.    end Gen;
   7.
   8.    function ABE return Integer;
   9.
  10.    function Cause_ABE return Boolean is
  11.       package Inst is new Gen (ABE);
            |
      >>> warning: in instantiation at line 5
      >>> warning: cannot call "ABE" before body seen
      >>> warning: Program_Error may be raised at run time
      >>> warning:   body of unit "Static_Model" elaborated
      >>> warning:   function "Cause_ABE" called at line 16
      >>> warning:   function "ABE" called at line 5, instance at line 11
  
  12.    begin
  13.       ...
  14.    end Cause_ABE;
  15.
  16.    Val : constant Boolean := Cause_ABE;
  17.
  18.    function ABE return Integer is
  19.    begin
  20.       ...
  21.    end ABE;
  22. end Static_Model;
  

  The example above illustrates an ABE problem within package Static_Model, which is hidden by several layers of indirection. The elaboration of package body Static_Model elaborates the declaration of Val. This invokes function Cause_ABE, which instantiates generic unit Gen as Inst. The elaboration of Inst invokes function ABE, however the body of ABE has not been elaborated yet.

• * `External targets'

  The static model installs run-time checks to verify the elaboration status of server targets only when the scenario that elaborates or executes that target is part of the elaboration code of the client unit. The checks can be suppressed using pragma Suppress (Elaboration_Check).

  with Server;
  package body Static_Model is
     generic
        with function Func return Integer;
     package Gen is
        Val : constant Integer := Func;
     end Gen;
  
     function Call_Func return Boolean is
        <check that the body of Server.Func is elaborated>
        package Inst is new Gen (Server.Func);
     begin
        ...
     end Call_Func;
  
     Val : constant Boolean := Call_Func;
  end Static_Model;
  

  In the example above, the elaboration of package body Static_Model elaborates the declaration of Val. This invokes function Call_Func, which instantiates generic unit Gen as Inst. The elaboration of Inst invokes function Server.Func. Since Server.Func is an external target, GNAT installs a run-time check to verify that its body has been elaborated.

  In addition to checks, the static model installs implicit Elaborate and Elaborate_All pragmas to guarantee safe elaboration use of server units. This information is available when compiler switch -gnatel is in effect.

   1. with Server;
   2. package body Static_Model is
   3.    generic
   4.       with function Func return Integer;
   5.    package Gen is
   6.       Val : constant Integer := Func;
   7.    end Gen;
   8.
   9.    function Call_Func return Boolean is
  10.       package Inst is new Gen (Server.Func);
            |
      >>> info: instantiation of "Gen" during elaboration
      >>> info: in instantiation at line 6
      >>> info: call to "Func" during elaboration
      >>> info: in instantiation at line 6
      >>> info: implicit pragma "Elaborate_All" generated for unit "Server"
      >>> info:   body of unit "Static_Model" elaborated
      >>> info:   function "Call_Func" called at line 15
      >>> info:   function "Func" called at line 6, instance at line 10
  
  11.    begin
  12.       ...
  13.    end Call_Func;
  14.
  15.    Val : constant Boolean := Call_Func;
                                   |
      >>> info: call to "Call_Func" during elaboration
  
  16. end Static_Model;
  

  In the example above, the elaboration of package body Static_Model elaborates the declaration of Val. This invokes function Call_Func, which instantiates generic unit Gen as Inst. The elaboration of Inst invokes function Server.Func. Since Server.Func is an external target, GNAT installs an implicit Elaborate_All pragma for unit Server. The pragma guarantees that both the spec and body of Server, along with any additional dependencies that Server may require, are elaborated prior to the body of Static_Model.