From a5740f2b7285f950e68d7790c37e28a5b768b4e8 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 3 Sep 2021 09:19:49 +0200 Subject: [PATCH] [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. --- gcc/ada/libgnat/a-textio.adb | 1 + gcc/ada/libgnat/a-textio.ads | 6 ++++-- 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 717f529a7bb5..8667360e2735 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 a06a35c50591..f94c92dff2cd 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 783c94aa53ea..3eee2ee31b73 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 -- 2.47.2