9.8 SPARK Diagnostics

GNAT enforces the SPARK rules of elaboration as defined in the SPARK Reference Manual section 7.7 when compiler switch -gnatd.v is in effect. Note that GNAT emits hard errors whenever it encounters a violation of the SPARK rules.

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

4. end SPARK_Diagnostics;