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 | |
| 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')
| -rw-r--r-- | gcc/ada/libgnat/a-textio.adb | 1 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-textio.ads | 6 | ||||
| -rw-r--r-- | gcc/ada/sem.adb | 9 |
3 files changed, 12 insertions, 4 deletions
diff --git a/gcc/ada/libgnat/a-textio.adb b/gcc/ada/libgnat/a-textio.adb index 717f529..8667360 100644 --- a/gcc/ada/libgnat/a-textio.adb +++ b/gcc/ada/libgnat/a-textio.adb @@ -44,6 +44,7 @@ pragma Elaborate_All (System.File_IO); -- Needed because of calls to Chain_File in package body elaboration package body Ada.Text_IO with + SPARK_Mode => Off, Refined_State => (File_System => (Standard_In, Standard_Out, Standard_Err, diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads index a06a35c..f94c92d 100644 --- a/gcc/ada/libgnat/a-textio.ads +++ b/gcc/ada/libgnat/a-textio.ads @@ -56,8 +56,9 @@ with System.File_Control_Block; with System.WCh_Con; package Ada.Text_IO with - Abstract_State => (File_System), - Initializes => (File_System), + SPARK_Mode, + Abstract_State => File_System, + Initializes => File_System, Initial_Condition => Line_Length = 0 and Page_Length = 0 is pragma Elaborate_Body; @@ -547,6 +548,7 @@ is Layout_Error : exception renames IO_Exceptions.Layout_Error; private + pragma SPARK_Mode (Off); -- The following procedures have a File_Type formal of mode IN OUT because -- they may close the original file. The Close operation may raise an 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 |