[Ada] Implement new rules for pragma SPARK_Mode

[Arnaud Charlet <charlet at adacore dot com>]

The rules for pragma SPARK_Mode have changed. In particular, the mode
is not inherited anymore from a the spec to the body, and the body
should not have a mode if the spec did not have one. These new rules
are checked now. A minor change is that SPARK_Mode is set even on
subprograms for which Comes_From_Source returns False (including
internal subprograms), as we need this information on subprograms
from instances of generics.

The following test now generates an error:

     1. package SPARKcode is
     2.    pragma SPARK_Mode (On);
     3.    procedure P1;
     4.    procedure P2 with SPARK_Mode => On;
     5.    procedure P3 with SPARK_Mode => Off;
     6. end SPARKcode;

     1. package body SPARKcode is
     2.    pragma SPARK_Mode (On);
     3.    procedure P1 is begin null; end;
     4.    procedure P2 is begin null; end;
     5.    procedure P3 is begin null; end;
           |
        >>> incorrect application of SPARK_Mode at line 2
        >>> value Off was set for SPARK_Mode on "P3" at sparkcode.ads:5

     6. end SPARKcode;

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

2014-01-29  Yannick Moy  <moy@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): SPARK_Mode
	not inherited from spec anymore. Check consistency
	rules after processing of declarations.
	* sem_ch7.adb (Analyze_Package_Body_Helper): SPARK_Mode not inherited
	from spec anymore. Check consistency rules after processing of
	declarations.
	(Analyze_Package_Declaration): Set SPARK_Mode only for non-generic
	packages.
	* sem_prag.adb (Analyze_Pragma/Pragma_SPARK_Mode): Implement new
	consistency rules.

Attachment: difs
Description: Text document