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

[Arnaud Charlet]

This patch clarifies the need of saving and restoring SPARK_Mode in a stack
like fashion. No change in behavior, no test needed.

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 comments on SPARK_Mode save/restore.
	* sem_ch7.adb (Analyze_Package_Body_Contract,
	Analyze_Package_Contract): Add comments on SPARK_Mode save/restore.

-------------- next part --------------
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 212721)
+++ sem_ch7.adb	(working copy)
@@ -184,6 +184,11 @@
       Prag    : Node_Id;
 
    begin
+      --  Due to the timing of contract analysis, delayed pragmas may be
+      --  subject to the wrong SPARK_Mode, usually that of the enclosing
+      --  context. To remedy this, restore the original SPARK_Mode of the
+      --  related package body.
+
       Save_SPARK_Mode_And_Set (Body_Id, Mode);
 
       Prag := Get_Pragma (Body_Id, Pragma_Refined_State);
@@ -204,6 +209,9 @@
          Error_Msg_N ("package & requires state refinement", Spec_Id);
       end if;
 
+      --  Restore the SPARK_Mode of the enclosing context after all delayed
+      --  pragmas have been analyzed.
+
       Restore_SPARK_Mode (Mode);
    end Analyze_Package_Body_Contract;
 
@@ -848,6 +856,11 @@
       Prag : Node_Id;
 
    begin
+      --  Due to the timing of contract analysis, delayed pragmas may be
+      --  subject to the wrong SPARK_Mode, usually that of the enclosing
+      --  context. To remedy this, restore the original SPARK_Mode of the
+      --  related package.
+
       Save_SPARK_Mode_And_Set (Pack_Id, Mode);
 
       --  Analyze the initialization related pragmas. Initializes must come
@@ -876,6 +889,9 @@
          end if;
       end if;
 
+      --  Restore the SPARK_Mode of the enclosing context after all delayed
+      --  pragmas have been analyzed.
+
       Restore_SPARK_Mode (Mode);
    end Analyze_Package_Contract;
 
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 212721)
+++ sem_ch6.adb	(working copy)
@@ -2040,6 +2040,11 @@
       Spec_Id     : Entity_Id;
 
    begin
+      --  Due to the timing of contract analysis, delayed pragmas may be
+      --  subject to the wrong SPARK_Mode, usually that of the enclosing
+      --  context. To remedy this, restore the original SPARK_Mode of the
+      --  related subprogram body.
+
       Save_SPARK_Mode_And_Set (Body_Id, Mode);
 
       --  When a subprogram body declaration is illegal, its defining entity is
@@ -2116,6 +2121,9 @@
          end if;
       end if;
 
+      --  Restore the SPARK_Mode of the enclosing context after all delayed
+      --  pragmas have been analyzed.
+
       Restore_SPARK_Mode (Mode);
    end Analyze_Subprogram_Body_Contract;
 
@@ -3693,6 +3701,11 @@
       Seen_In_Post : Boolean := False;
 
    begin
+      --  Due to the timing of contract analysis, delayed pragmas may be
+      --  subject to the wrong SPARK_Mode, usually that of the enclosing
+      --  context. To remedy this, restore the original SPARK_Mode of the
+      --  related subprogram body.
+
       Save_SPARK_Mode_And_Set (Subp, Mode);
 
       if Present (Items) then
@@ -3817,6 +3830,9 @@
          end if;
       end if;
 
+      --  Restore the SPARK_Mode of the enclosing context after all delayed
+      --  pragmas have been analyzed.
+
       Restore_SPARK_Mode (Mode);
    end Analyze_Subprogram_Contract;