From: Arnaud Charlet <charlet@gcc.gnu.org>
Date: Fri, 18 Jul 2014 15:39:59 +0000 (+0200)
Subject: Update comments
X-Git-Tag: releases/gcc-5.1.0~6210
X-Git-Url: http://git.ipfire.org/gitweb.cgi?a=commitdiff_plain;h=efd3c368ab6b0da227c1b893ce9f411970f89ddc;p=thirdparty%2Fgcc.git

Update comments

From-SVN: r212819
---

diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 372fd86ce6fe..099bbd74d10a 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -184,6 +184,11 @@ package body Sem_Ch7 is
       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 @@ package body Sem_Ch7 is
          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 @@ package body Sem_Ch7 is
       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 @@ package body Sem_Ch7 is
          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;