diff options
author | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-07-18 17:39:59 +0200 |
---|---|---|
committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-07-18 17:39:59 +0200 |
commit | efd3c368ab6b0da227c1b893ce9f411970f89ddc (patch) | |
tree | 6d2ffd86097ca457f66f3642d1694c3220e33e48 /gcc | |
parent | 4b03d946237dd6a6953dd1337043cd9eb8e7fbcb (diff) | |
download | gcc-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.adb | 16 |
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; |