[Ada] Analysis of delayed SPARK aspects and use of SPARK_Mode

[Arnaud Charlet <charlet at adacore dot com>]

This patch ensures that all delayed SPARK aspects are analyzed with the proper
SPARK mode of their related construct.

------------
-- Source --
------------

--  modes.ads

package Modes
  with SPARK_Mode => On,
       Abstract_State => State
is
   Var : Integer := 1;

   procedure Disabled_1 (Formal : Integer)
     with SPARK_Mode => Off,
          Global  => (Input => (Formal, State, Var)),  --  suppressed
          Depends => (null  => (Formal, Var));         --  suppressed

   procedure Enabled_1 (Formal : Integer)
     with SPARK_Mode => On,
          Global  => (Input => (Formal, State, Var)),  --  error
          Depends => (null  => (Formal, Var));         --  error
end Modes;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c modes.ads
modes.ads:14:33: global item cannot reference parameter of subprogram
modes.ads:14:41: state "State" must appear in at least one input dependence
  list

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

2014-07-17  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Contract,
	Analyze_Subprogram_Contract): Add new local variable Mode. Save
	and restore the SPARK mode of the related construct in a
	stack-like fashion.
	* sem_ch7.adb (Analyze_Package_Body_Contract,
	Analyze_Package_Contract): Add new local variable Mode. Save and
	restore the SPARK mode of the related construct in a stack-like fashion.
	* sem_util.adb Remove with and use clause for Opt.
	(Restore_SPARK_Mode): New routine.
	(Save_SPARK_Mode_And_Set): New routine.
	* sem_util.ads Add with and use clause for Opt.
	(Restore_SPARK_Mode): New routine.
	(Save_SPARK_Mode_And_Set): New routine.

Attachment: difs
Description: Text document