[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.

diff --git a/gcc/ada/libgnat/a-textio.adb b/gcc/ada/libgnat/a-textio.adb
index 717f529a7bb54abae74c3eb59a9bc1ed5aa855dc..8667360e2735e8743890888fda9f7bc393f3e95f 100644 (file)
--- 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 a06a35c50591d5800555387b8bdc1e3a310f37c6..f94c92dff2cd242a2466b6570c5505dcb4a92999 100644 (file)
--- 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 783c94aa53eaee9b4893d9e4ff5ffc16689bce9c..3eee2ee31b73e61ff248f92dec63ce2c0a079d5e 100644 (file)
--- 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