Next: , Previous: , Up: Elaboration Order Handling in GNAT   [Contents][Index]

9.9 SPARK Elaboration Model in GNAT

The SPARK model is identical to the static model in its handling of internal targets. The SPARK model, however, requires explicit Elaborate or Elaborate_All pragmas to be present in the program when a target is external, and compiler switch -gnatd.v is in effect. 

1. with Server;
2. package body SPARK_Model with SPARK_Mode is
3.    Val : constant Integer := Server.Func;
                                      |
   >>> call to "Func" during elaboration in SPARK
   >>> unit "SPARK_Model" requires pragma "Elaborate_All" for "Server"
   >>>   body of unit "SPARK_Model" elaborated
   >>>   function "Func" called at line 3

4. end SPARK_Model;