[Ada] Add warning for Suppress (Elaboration_Check) in SPARK

[Arnaud Charlet <charlet at adacore dot com>]

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  <dewar@adacore.com>

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

Attachment: difs
Description: Text document