diff options
| author | Yannick Moy <moy@adacore.com> | 2021-09-03 09:19:49 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-10-04 08:45:10 +0000 |
| commit | a5740f2b7285f950e68d7790c37e28a5b768b4e8 (patch) | |
| tree | 38a8dee53c0fd9be033acf6155bf44d54b9e58bd /gcc/ada/sem.adb | |
| parent | 39d7ff0fd7487bfb188f9e4c186076a106f995f8 (diff) | |
| download | gcc-a5740f2b7285f950e68d7790c37e28a5b768b4e8.zip gcc-a5740f2b7285f950e68d7790c37e28a5b768b4e8.tar.gz gcc-a5740f2b7285f950e68d7790c37e28a5b768b4e8.tar.bz2 | |
[Ada] Mark Ada.Text_IO in SPARK
gcc/ada/
* libgnat/a-textio.adb: Mark body out of SPARK.
* libgnat/a-textio.ads: Mark spec in SPARK and private part out
of SPARK.
* sem.adb (Semantics.Do_Analyze): Similar to ghost code
attributes, save and restore value of
Ignore_SPARK_Mode_Pragmas_In_Instance.
Diffstat (limited to 'gcc/ada/sem.adb')
| -rw-r--r-- | gcc/ada/sem.adb | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index 783c94aa..3eee2ee 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.adb @@ -1402,7 +1402,9 @@ package body Sem is procedure Do_Analyze is Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; Saved_IGR : constant Node_Id := Ignored_Ghost_Region; - -- Save the Ghost-related attributes to restore on exit + Saved_ISMP : constant Boolean := + Ignore_SPARK_Mode_Pragmas_In_Instance; + -- Save Ghost and SPARK mode-related data to restore on exit -- Generally style checks are preserved across compilations, with -- one exception: s-oscons.ads, which allows arbitrary long lines @@ -1421,6 +1423,7 @@ package body Sem is -- Set up a clean environment before analyzing Install_Ghost_Region (None, Empty); + Ignore_SPARK_Mode_Pragmas_In_Instance := False; Outer_Generic_Scope := Empty; Scope_Suppress := Suppress_Options; @@ -1443,9 +1446,11 @@ package body Sem is Pop_Scope; Restore_Scope_Stack (List); - Restore_Ghost_Region (Saved_GM, Saved_IGR); Style_Max_Line_Length := Saved_ML; Style_Check_Max_Line_Length := Saved_CML; + + Restore_Ghost_Region (Saved_GM, Saved_IGR); + Ignore_SPARK_Mode_Pragmas_In_Instance := Saved_ISMP; end Do_Analyze; -- Local variables |