Now that access-to-constant types are supported in SPARK, type
File_Access is accepted and the public interface of Ada.Text_IO can be
marked in SPARK.
Fix a missing save/restore for the global variable storing whether
SPARK_Mode should be ignored inside instances, around the analysis of a
new unit (e.g. from a with_clause).
Tested on x86_64-pc-linux-gnu, committed on trunk
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
--- 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
--- 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
--- 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
