aboutsummaryrefslogtreecommitdiff
path: root/gcc
diff options
context:
space:
mode:
authorArnaud Charlet <charlet@gcc.gnu.org>2014-07-18 17:39:59 +0200
committerArnaud Charlet <charlet@gcc.gnu.org>2014-07-18 17:39:59 +0200
commitefd3c368ab6b0da227c1b893ce9f411970f89ddc (patch)
tree6d2ffd86097ca457f66f3642d1694c3220e33e48 /gcc
parent4b03d946237dd6a6953dd1337043cd9eb8e7fbcb (diff)
downloadgcc-efd3c368ab6b0da227c1b893ce9f411970f89ddc.zip
gcc-efd3c368ab6b0da227c1b893ce9f411970f89ddc.tar.gz
gcc-efd3c368ab6b0da227c1b893ce9f411970f89ddc.tar.bz2
Update comments
From-SVN: r212819
Diffstat (limited to 'gcc')
-rw-r--r--gcc/ada/sem_ch7.adb16
1 files changed, 16 insertions, 0 deletions
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 372fd86..099bbd7 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;