SPARK Diagnostics (GNAT User’s Guide for Native Platforms)

### 9.8 SPARK Diagnostics ¶

GNAT enforces the SPARK rules of elaboration as defined in the SPARK Reference Manual section 7.7 when you specify compiler switch `-gnatd.v`. Note that GNAT emits 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;