diff options
| author | Yannick Moy <moy@adacore.com> | 2020-01-10 14:46:25 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-06-03 06:01:39 -0400 |
| commit | 93b3110d75423001107785967a9f9c962e96d2e9 (patch) | |
| tree | c8294a0e8410e803d0f1c78eb1b9726393bc9894 /gcc/ada/rtsfind.adb | |
| parent | e60b6e23741c6d6059e6f765f18ce4c56366874b (diff) | |
| download | gcc-93b3110d75423001107785967a9f9c962e96d2e9.zip gcc-93b3110d75423001107785967a9f9c962e96d2e9.tar.gz gcc-93b3110d75423001107785967a9f9c962e96d2e9.tar.bz2 | |
[Ada] Improve handling of SPARK_Mode in generic instances
2020-06-03 Yannick Moy <moy@adacore.com>
gcc/ada/
* rtsfind.adb (Load_RTU): Correctly set/reset global variable to
ignore SPARK_Mode in instances around loading.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Accept Off
without prior On.
* sem_ch7.adb (Analyze_Package_Body_Helper): Likewise.
* sem_prag.adb (Analyze_Pragma): Always take into account
SPARK_Mode Off.
Diffstat (limited to 'gcc/ada/rtsfind.adb')
| -rw-r--r-- | gcc/ada/rtsfind.adb | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb index 18b828e..14371b4 100644 --- a/gcc/ada/rtsfind.adb +++ b/gcc/ada/rtsfind.adb @@ -931,6 +931,8 @@ package body Rtsfind is Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + Saved_ISMP : constant Boolean := + Ignore_SPARK_Mode_Pragmas_In_Instance; Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; -- Save Ghost and SPARK mode-related data to restore on exit @@ -946,6 +948,7 @@ package body Rtsfind is -- Provide a clean environment for the unit + Ignore_SPARK_Mode_Pragmas_In_Instance := False; Install_Ghost_Region (None, Empty); Install_SPARK_Mode (None, Empty); @@ -1044,6 +1047,7 @@ package body Rtsfind is Set_Is_Potentially_Use_Visible (U.Entity, True); end if; + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; Restore_Ghost_Region (Saved_GM, Saved_IGR); Restore_SPARK_Mode (Saved_SM, Saved_SMP); end Load_RTU; |