From: Joffrey Huguet Date: Fri, 5 Jul 2019 07:03:44 +0000 (+0000) Subject: [Ada] Add contracts to Ada.Text_IO for SPARK X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2ff7c604377c1220702aeb4c4b63ed76e56aa577;p=gcc.git [Ada] Add contracts to Ada.Text_IO for SPARK This change removes the warnings returned when using Ada.Text_IO library in SPARK. An abstract state and global contracts were added to modelize the action of Text_IO procedures and function on the memory and the files. 2019-07-05 Joffrey Huguet gcc/ada/ * libgnat/a-textio.adb: Add abstract state refinment. * libgnat/a-textio.ads: Add File_System abstract state. Add global contracts, contract cases, preconditions and postconditions to procedures and functions. (Set_Input, Set_Output, Set_Error, Standard_Input, Standard_Output, Standard_Error, Current_Input, Current_Output, Current_Error): Turn SPARK_Mode off. (Get_Line): Turn SPARK_Mode off on Get_Line functions. * libgnat/a-tideio.ads, libgnat/a-tienio.ads, libgnat/a-tifiio.ads, libgnat/a-tiflio.ads, libgnat/a-tiinio.ads, libgnat/a-timoio.ads: Add global contracts, contract cases, preconditions and postconditions to procedures and functions. From-SVN: r273127 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 002d535c450..882011336c1 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,19 @@ +2019-07-05 Joffrey Huguet + + * libgnat/a-textio.adb: Add abstract state refinment. + * libgnat/a-textio.ads: Add File_System abstract state. Add + global contracts, contract cases, preconditions and + postconditions to procedures and functions. + (Set_Input, Set_Output, Set_Error, Standard_Input, + Standard_Output, Standard_Error, Current_Input, Current_Output, + Current_Error): Turn SPARK_Mode off. + (Get_Line): Turn SPARK_Mode off on Get_Line functions. + * libgnat/a-tideio.ads, libgnat/a-tienio.ads, + libgnat/a-tifiio.ads, libgnat/a-tiflio.ads, + libgnat/a-tiinio.ads, libgnat/a-timoio.ads: Add global + contracts, contract cases, preconditions and postconditions to + procedures and functions. + 2019-07-05 Arnaud Charlet * doc/gnat_ugn/platform_specific_information.rst: Refresh doc on diff --git a/gcc/ada/libgnat/a-textio.adb b/gcc/ada/libgnat/a-textio.adb index 5b6e28a5341..276be122c09 100644 --- a/gcc/ada/libgnat/a-textio.adb +++ b/gcc/ada/libgnat/a-textio.adb @@ -43,7 +43,18 @@ with Ada.Unchecked_Deallocation; pragma Elaborate_All (System.File_IO); -- Needed because of calls to Chain_File in package body elaboration -package body Ada.Text_IO is +package body Ada.Text_IO with + Refined_State => (File_System => (Standard_In, + Standard_Out, + Standard_Err, + Current_In, + Current_Out, + Current_Err, + In_Name, + Out_Name, + Err_Name, + WC_Encoding)) +is package FIO renames System.File_IO; diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads index 32bbc6cb6a0..a2e1daf043e 100644 --- a/gcc/ada/libgnat/a-textio.ads +++ b/gcc/ada/libgnat/a-textio.ads @@ -33,6 +33,14 @@ -- -- ------------------------------------------------------------------------------ +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. These preconditions +-- are partial and protect against Status_Error, Mode_Error, and Layout_Error, +-- but not against other types of errors. + +pragma Assertion_Policy (Pre => Ignore); + -- Note: the generic subpackages of Text_IO (Integer_IO, Float_IO, Fixed_IO, -- Modular_IO, Decimal_IO and Enumeration_IO) appear as private children in -- GNAT. These children are with'ed automatically if they are referenced, so @@ -46,10 +54,15 @@ with System; with System.File_Control_Block; with System.WCh_Con; -package Ada.Text_IO is +package Ada.Text_IO with + Abstract_State => (File_System), + Initializes => (File_System), + Initial_Condition => Line_Length = 0 and Page_Length = 0 +is pragma Elaborate_Body; - type File_Type is limited private with Default_Initial_Condition; + type File_Type is limited private with + Default_Initial_Condition => (not Is_Open (File_Type)); type File_Mode is (In_File, Out_File, Append_File); -- The following representation clause allows the use of unchecked @@ -87,50 +100,97 @@ package Ada.Text_IO is (File : in out File_Type; Mode : File_Mode := Out_File; Name : String := ""; - Form : String := ""); + Form : String := "") + with + Pre => not Is_Open (File), + Post => + Is_Open (File) + and then Ada.Text_IO.Mode (File) = Mode + and then (if Mode /= In_File + then (Line_Length (File) = 0 + and then Page_Length (File) = 0)), + Global => (In_Out => File_System); procedure Open (File : in out File_Type; Mode : File_Mode; Name : String; - Form : String := ""); - - procedure Close (File : in out File_Type); - procedure Delete (File : in out File_Type); - procedure Reset (File : in out File_Type; Mode : File_Mode); - procedure Reset (File : in out File_Type); - - function Mode (File : File_Type) return File_Mode; - function Name (File : File_Type) return String; - function Form (File : File_Type) return String; - - function Is_Open (File : File_Type) return Boolean; + Form : String := "") + with + Pre => not Is_Open (File), + Post => + Is_Open (File) + and then Ada.Text_IO.Mode (File) = Mode + and then (if Mode /= In_File + then (Line_Length (File) = 0 + and then Page_Length (File) = 0)), + Global => (In_Out => File_System); + + procedure Close (File : in out File_Type) with + Pre => Is_Open (File), + Post => not Is_Open (File), + Global => (In_Out => File_System); + procedure Delete (File : in out File_Type) with + Pre => Is_Open (File), + Post => not Is_Open (File), + Global => (In_Out => File_System); + procedure Reset (File : in out File_Type; Mode : File_Mode) with + Pre => Is_Open (File), + Post => + Is_Open (File) + and then Ada.Text_IO.Mode (File) = Mode + and then (if Mode /= In_File + then (Line_Length (File) = 0 + and then Page_Length (File) = 0)), + Global => (In_Out => File_System); + procedure Reset (File : in out File_Type) with + Pre => Is_Open (File), + Post => + Is_Open (File) + and Mode (File)'Old = Mode (File) + and (if Mode (File) /= In_File + then (Line_Length (File) = 0 + and then Page_Length (File) = 0)), + Global => (In_Out => File_System); + + function Mode (File : File_Type) return File_Mode with + Pre => Is_Open (File), + Global => null; + function Name (File : File_Type) return String with + Pre => Is_Open (File), + Global => null; + function Form (File : File_Type) return String with + Pre => Is_Open (File), + Global => null; + + function Is_Open (File : File_Type) return Boolean with + Global => null; ------------------------------------------------------ -- Control of default input, output and error files -- ------------------------------------------------------ - procedure Set_Input (File : File_Type); - procedure Set_Output (File : File_Type); - procedure Set_Error (File : File_Type); + procedure Set_Input (File : File_Type) with SPARK_Mode => Off; + procedure Set_Output (File : File_Type) with SPARK_Mode => Off; + procedure Set_Error (File : File_Type) with SPARK_Mode => Off; - function Standard_Input return File_Type; - function Standard_Output return File_Type; - function Standard_Error return File_Type; + function Standard_Input return File_Type with SPARK_Mode => Off; + function Standard_Output return File_Type with SPARK_Mode => Off; + function Standard_Error return File_Type with SPARK_Mode => Off; - function Current_Input return File_Type; - function Current_Output return File_Type; - function Current_Error return File_Type; + function Current_Input return File_Type with SPARK_Mode => Off; + function Current_Output return File_Type with SPARK_Mode => Off; + function Current_Error return File_Type with SPARK_Mode => Off; type File_Access is access constant File_Type; - function Standard_Input return File_Access; - function Standard_Output return File_Access; - function Standard_Error return File_Access; + function Standard_Input return File_Access with SPARK_Mode => Off; + function Standard_Output return File_Access with SPARK_Mode => Off; + function Standard_Error return File_Access with SPARK_Mode => Off; - function Current_Input return File_Access; - function Current_Output return File_Access; - function Current_Error return File_Access; + function Current_Input return File_Access with SPARK_Mode => Off; + function Current_Output return File_Access with SPARK_Mode => Off; + function Current_Error return File_Access with SPARK_Mode => Off; -------------------- -- Buffer control -- @@ -139,129 +199,319 @@ package Ada.Text_IO is -- Note: The parameter file is IN OUT in the RM, but this is clearly -- an oversight, and was intended to be IN, see AI95-00057. - procedure Flush (File : File_Type); - procedure Flush; + procedure Flush (File : File_Type) with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); + procedure Flush with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); -------------------------------------------- -- Specification of line and page lengths -- -------------------------------------------- - procedure Set_Line_Length (File : File_Type; To : Count); - procedure Set_Line_Length (To : Count); - - procedure Set_Page_Length (File : File_Type; To : Count); - procedure Set_Page_Length (To : Count); - - function Line_Length (File : File_Type) return Count; - function Line_Length return Count; - - function Page_Length (File : File_Type) return Count; - function Page_Length return Count; + procedure Set_Line_Length (File : File_Type; To : Count) with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File) = To + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); + procedure Set_Line_Length (To : Count) with + Post => + Line_Length = To + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); + + procedure Set_Page_Length (File : File_Type; To : Count) with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Page_Length (File) = To + and Line_Length (File)'Old = Line_Length (File), + Global => (In_Out => File_System); + procedure Set_Page_Length (To : Count) with + Post => + Page_Length = To + and Line_Length'Old = Line_Length, + Global => (In_Out => File_System); + + function Line_Length (File : File_Type) return Count with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Global => (Input => File_System); + function Line_Length return Count with + Global => (Input => File_System); + + function Page_Length (File : File_Type) return Count with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Global => (Input => File_System); + function Page_Length return Count with + Global => (Input => File_System); ------------------------------------ -- Column, Line, and Page Control -- ------------------------------------ - procedure New_Line (File : File_Type; Spacing : Positive_Count := 1); - procedure New_Line (Spacing : Positive_Count := 1); - - procedure Skip_Line (File : File_Type; Spacing : Positive_Count := 1); - procedure Skip_Line (Spacing : Positive_Count := 1); - - function End_Of_Line (File : File_Type) return Boolean; - function End_Of_Line return Boolean; - - procedure New_Page (File : File_Type); - procedure New_Page; - - procedure Skip_Page (File : File_Type); - procedure Skip_Page; - - function End_Of_Page (File : File_Type) return Boolean; - function End_Of_Page return Boolean; - - function End_Of_File (File : File_Type) return Boolean; - function End_Of_File return Boolean; - - procedure Set_Col (File : File_Type; To : Positive_Count); - procedure Set_Col (To : Positive_Count); - - procedure Set_Line (File : File_Type; To : Positive_Count); - procedure Set_Line (To : Positive_Count); - - function Col (File : File_Type) return Positive_Count; - function Col return Positive_Count; - - function Line (File : File_Type) return Positive_Count; - function Line return Positive_Count; - - function Page (File : File_Type) return Positive_Count; - function Page return Positive_Count; + procedure New_Line (File : File_Type; Spacing : Positive_Count := 1) with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); + procedure New_Line (Spacing : Positive_Count := 1) with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); + + procedure Skip_Line (File : File_Type; Spacing : Positive_Count := 1) with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); + procedure Skip_Line (Spacing : Positive_Count := 1) with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); + + function End_Of_Line (File : File_Type) return Boolean with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System); + function End_Of_Line return Boolean with + Global => (Input => File_System); + + procedure New_Page (File : File_Type) with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); + procedure New_Page with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); + + procedure Skip_Page (File : File_Type) with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); + procedure Skip_Page with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); + + function End_Of_Page (File : File_Type) return Boolean with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System); + function End_Of_Page return Boolean with + Global => (Input => File_System); + + function End_Of_File (File : File_Type) return Boolean with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System); + function End_Of_File return Boolean with + Global => (Input => File_System); + + procedure Set_Col (File : File_Type; To : Positive_Count) with + Pre => + Is_Open (File) + and then (if Mode (File) /= In_File + then (Line_Length (File) = 0 + or else To <= Line_Length (File))), + Contract_Cases => + (Mode (File) /= In_File => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + others => True), + Global => (In_Out => File_System); + procedure Set_Col (To : Positive_Count) with + Pre => Line_Length = 0 or To <= Line_Length, + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); + + procedure Set_Line (File : File_Type; To : Positive_Count) with + Pre => + Is_Open (File) + and then (if Mode (File) /= In_File + then (Page_Length (File) = 0 + or else To <= Page_Length (File))), + Contract_Cases => + (Mode (File) /= In_File => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + others => True), + Global => (In_Out => File_System); + procedure Set_Line (To : Positive_Count) with + Pre => Page_Length = 0 or To <= Page_Length, + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); + + function Col (File : File_Type) return Positive_Count with + Pre => Is_Open (File), + Global => (Input => File_System); + function Col return Positive_Count with + Global => (Input => File_System); + + function Line (File : File_Type) return Positive_Count with + Pre => Is_Open (File), + Global => (Input => File_System); + function Line return Positive_Count with + Global => (Input => File_System); + + function Page (File : File_Type) return Positive_Count with + Pre => Is_Open (File), + Global => (Input => File_System); + function Page return Positive_Count with + Global => (Input => File_System); ---------------------------- -- Character Input-Output -- ---------------------------- - procedure Get (File : File_Type; Item : out Character); - procedure Get (Item : out Character); - procedure Put (File : File_Type; Item : Character); - procedure Put (Item : Character); + procedure Get (File : File_Type; Item : out Character) with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); + procedure Get (Item : out Character) with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); + procedure Put (File : File_Type; Item : Character) with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); + procedure Put (Item : Character) with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Look_Ahead (File : File_Type; Item : out Character; - End_Of_Line : out Boolean); + End_Of_Line : out Boolean) + with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System); procedure Look_Ahead (Item : out Character; - End_Of_Line : out Boolean); + End_Of_Line : out Boolean) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (Input => File_System); procedure Get_Immediate (File : File_Type; - Item : out Character); + Item : out Character) + with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); procedure Get_Immediate - (Item : out Character); + (Item : out Character) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Get_Immediate (File : File_Type; Item : out Character; - Available : out Boolean); + Available : out Boolean) + with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); procedure Get_Immediate (Item : out Character; - Available : out Boolean); + Available : out Boolean) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); ------------------------- -- String Input-Output -- ------------------------- - procedure Get (File : File_Type; Item : out String); - procedure Get (Item : out String); - procedure Put (File : File_Type; Item : String); - procedure Put (Item : String); + procedure Get (File : File_Type; Item : out String) with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); + procedure Get (Item : out String) with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); + procedure Put (File : File_Type; Item : String) with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); + procedure Put (Item : String) with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Get_Line (File : File_Type; Item : out String; - Last : out Natural); + Last : out Natural) + with + Pre => Is_Open (File) and then Mode (File) = In_File, + Post => (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last + else Last = Item'First - 1), + Global => (In_Out => File_System); procedure Get_Line (Item : out String; - Last : out Natural); - - function Get_Line (File : File_Type) return String; + Last : out Natural) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length + and (if Item'Length > 0 then Last in Item'First - 1 .. Item'Last + else Last = Item'First - 1), + Global => (In_Out => File_System); + + function Get_Line (File : File_Type) return String with SPARK_Mode => Off; pragma Ada_05 (Get_Line); - function Get_Line return String; + function Get_Line return String with SPARK_Mode => Off; pragma Ada_05 (Get_Line); procedure Put_Line (File : File_Type; - Item : String); + Item : String) + with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); procedure Put_Line - (Item : String); + (Item : String) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); --------------------------------------- -- Generic packages for Input-Output -- @@ -447,14 +697,20 @@ private Standard_Out_AFCB : aliased Text_AFCB; Standard_Err_AFCB : aliased Text_AFCB; - Standard_In : aliased File_Type := Standard_In_AFCB'Access; - Standard_Out : aliased File_Type := Standard_Out_AFCB'Access; - Standard_Err : aliased File_Type := Standard_Err_AFCB'Access; + Standard_In : aliased File_Type := Standard_In_AFCB'Access with + Part_Of => File_System; + Standard_Out : aliased File_Type := Standard_Out_AFCB'Access with + Part_Of => File_System; + Standard_Err : aliased File_Type := Standard_Err_AFCB'Access with + Part_Of => File_System; -- Standard files - Current_In : aliased File_Type := Standard_In; - Current_Out : aliased File_Type := Standard_Out; - Current_Err : aliased File_Type := Standard_Err; + Current_In : aliased File_Type := Standard_In with + Part_Of => File_System; + Current_Out : aliased File_Type := Standard_Out with + Part_Of => File_System; + Current_Err : aliased File_Type := Standard_Err with + Part_Of => File_System; -- Current files function EOF_Char return Integer; diff --git a/gcc/ada/libgnat/a-tideio.ads b/gcc/ada/libgnat/a-tideio.ads index c504707b665..efe52c565d2 100644 --- a/gcc/ada/libgnat/a-tideio.ads +++ b/gcc/ada/libgnat/a-tideio.ads @@ -52,35 +52,58 @@ package Ada.Text_IO.Decimal_IO is procedure Get (File : File_Type; Item : out Num; - Width : Field := 0); + Width : Field := 0) + with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); procedure Get (Item : out Num; - Width : Field := 0); + Width : Field := 0) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Put (File : File_Type; Item : Num; Fore : Field := Default_Fore; Aft : Field := Default_Aft; - Exp : Field := Default_Exp); + Exp : Field := Default_Exp) + with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); procedure Put (Item : Num; Fore : Field := Default_Fore; Aft : Field := Default_Aft; - Exp : Field := Default_Exp); + Exp : Field := Default_Exp) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Get (From : String; Item : out Num; - Last : out Positive); + Last : out Positive) + with + Global => null; procedure Put (To : out String; Item : Num; Aft : Field := Default_Aft; - Exp : Field := Default_Exp); + Exp : Field := Default_Exp) + with + Global => null; private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tienio.ads b/gcc/ada/libgnat/a-tienio.ads index 68f4694321b..fb80abdf8ff 100644 --- a/gcc/ada/libgnat/a-tienio.ads +++ b/gcc/ada/libgnat/a-tienio.ads @@ -28,28 +28,49 @@ package Ada.Text_IO.Enumeration_IO is Default_Width : Field := 0; Default_Setting : Type_Set := Upper_Case; - procedure Get (File : File_Type; Item : out Enum); - procedure Get (Item : out Enum); + procedure Get (File : File_Type; Item : out Enum) with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); + procedure Get (Item : out Enum) with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Put (File : File_Type; Item : Enum; Width : Field := Default_Width; - Set : Type_Set := Default_Setting); + Set : Type_Set := Default_Setting) + with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); procedure Put (Item : Enum; Width : Field := Default_Width; - Set : Type_Set := Default_Setting); + Set : Type_Set := Default_Setting) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Get (From : String; Item : out Enum; - Last : out Positive); + Last : out Positive) + with + Global => null; procedure Put (To : out String; Item : Enum; - Set : Type_Set := Default_Setting); + Set : Type_Set := Default_Setting) + with + Global => null; end Ada.Text_IO.Enumeration_IO; diff --git a/gcc/ada/libgnat/a-tifiio.ads b/gcc/ada/libgnat/a-tifiio.ads index 265600dbe46..1acf67ab760 100644 --- a/gcc/ada/libgnat/a-tifiio.ads +++ b/gcc/ada/libgnat/a-tifiio.ads @@ -32,35 +32,58 @@ package Ada.Text_IO.Fixed_IO is procedure Get (File : File_Type; Item : out Num; - Width : Field := 0); + Width : Field := 0) + with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); procedure Get (Item : out Num; - Width : Field := 0); + Width : Field := 0) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Put (File : File_Type; Item : Num; Fore : Field := Default_Fore; Aft : Field := Default_Aft; - Exp : Field := Default_Exp); + Exp : Field := Default_Exp) + with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); procedure Put (Item : Num; Fore : Field := Default_Fore; Aft : Field := Default_Aft; - Exp : Field := Default_Exp); + Exp : Field := Default_Exp) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Get (From : String; Item : out Num; - Last : out Positive); + Last : out Positive) + with + Global => null; procedure Put (To : out String; Item : Num; Aft : Field := Default_Aft; - Exp : Field := Default_Exp); + Exp : Field := Default_Exp) + with + Global => null; private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tiflio.ads b/gcc/ada/libgnat/a-tiflio.ads index dcc4856bea8..16e65a55de2 100644 --- a/gcc/ada/libgnat/a-tiflio.ads +++ b/gcc/ada/libgnat/a-tiflio.ads @@ -52,35 +52,58 @@ package Ada.Text_IO.Float_IO is procedure Get (File : File_Type; Item : out Num; - Width : Field := 0); + Width : Field := 0) + with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); procedure Get (Item : out Num; - Width : Field := 0); + Width : Field := 0) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Put (File : File_Type; Item : Num; Fore : Field := Default_Fore; Aft : Field := Default_Aft; - Exp : Field := Default_Exp); + Exp : Field := Default_Exp) + with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); procedure Put (Item : Num; Fore : Field := Default_Fore; Aft : Field := Default_Aft; - Exp : Field := Default_Exp); + Exp : Field := Default_Exp) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Get (From : String; Item : out Num; - Last : out Positive); + Last : out Positive) + with + Global => null; procedure Put (To : out String; Item : Num; Aft : Field := Default_Aft; - Exp : Field := Default_Exp); + Exp : Field := Default_Exp) + with + Global => null; private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-tiinio.ads b/gcc/ada/libgnat/a-tiinio.ads index 429f3b183ba..28f8d54abf7 100644 --- a/gcc/ada/libgnat/a-tiinio.ads +++ b/gcc/ada/libgnat/a-tiinio.ads @@ -51,32 +51,55 @@ package Ada.Text_IO.Integer_IO is procedure Get (File : File_Type; Item : out Num; - Width : Field := 0); + Width : Field := 0) + with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); procedure Get (Item : out Num; - Width : Field := 0); + Width : Field := 0) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Put (File : File_Type; Item : Num; Width : Field := Default_Width; - Base : Number_Base := Default_Base); + Base : Number_Base := Default_Base) + with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); procedure Put (Item : Num; Width : Field := Default_Width; - Base : Number_Base := Default_Base); + Base : Number_Base := Default_Base) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Get (From : String; Item : out Num; - Last : out Positive); + Last : out Positive) + with + Global => null; procedure Put (To : out String; Item : Num; - Base : Number_Base := Default_Base); + Base : Number_Base := Default_Base) + with + Global => null; private pragma Inline (Get); diff --git a/gcc/ada/libgnat/a-timoio.ads b/gcc/ada/libgnat/a-timoio.ads index 5b8a72ebf1b..2d1ab91d4a4 100644 --- a/gcc/ada/libgnat/a-timoio.ads +++ b/gcc/ada/libgnat/a-timoio.ads @@ -51,32 +51,55 @@ package Ada.Text_IO.Modular_IO is procedure Get (File : File_Type; Item : out Num; - Width : Field := 0); + Width : Field := 0) + with + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System); procedure Get (Item : out Num; - Width : Field := 0); + Width : Field := 0) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Put (File : File_Type; Item : Num; Width : Field := Default_Width; - Base : Number_Base := Default_Base); + Base : Number_Base := Default_Base) + with + Pre => Is_Open (File) and then Mode (File) /= In_File, + Post => + Line_Length (File)'Old = Line_Length (File) + and Page_Length (File)'Old = Page_Length (File), + Global => (In_Out => File_System); procedure Put (Item : Num; Width : Field := Default_Width; - Base : Number_Base := Default_Base); + Base : Number_Base := Default_Base) + with + Post => + Line_Length'Old = Line_Length + and Page_Length'Old = Page_Length, + Global => (In_Out => File_System); procedure Get (From : String; Item : out Num; - Last : out Positive); + Last : out Positive) + with + Global => null; procedure Put (To : out String; Item : Num; - Base : Number_Base := Default_Base); + Base : Number_Base := Default_Base) + with + Global => null; private pragma Inline (Get);