The SPARK model is identical to the static model in its handling of internal
targets. The SPARK model, however, requires explicit
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;