This adds an additional warning message for Suppress (Elaboration_Check)
in SPARK mode:

The following is compiled with -gnatj55

     1. pragma SPARK_Mode (On);
     2. package SupEcheck is
     3.    pragma Suppress (Elaboration_Check);
                            |
        >>> warning: Suppress of Elaboration_Check
            ignored in SPARK, elaboration checking
            rules are statically enforced (SPARK RM
            7.7)

     4.    X : Integer;
     5. end;

Tested on x86_64-pc-linux-gnu, committed on trunk

2015-01-06  Robert Dewar  <de...@adacore.com>

        * sem_prag.adb (Process_Suppress_Unsuppress): Add extra warning
        for ignoring pragma Suppress (Elaboration_Check) in SPARK mode.

Index: sem_prag.adb
===================================================================
--- sem_prag.adb        (revision 219222)
+++ sem_prag.adb        (working copy)
@@ -9050,7 +9050,9 @@
 
          if C = Elaboration_Check and then SPARK_Mode = On then
             Error_Pragma_Arg
-              ("Suppress of Elaboration_Check ignored in SPARK??", Arg1);
+              ("Suppress of Elaboration_Check ignored in SPARK??",
+               "\elaboration checking rules are statically enforced "
+               & "(SPARK RM 7.7)", Arg1);
          end if;
 
          --  One-argument case

Reply via email to