diff options
Diffstat (limited to 'gcc/ada/libgnat/a-textio.ads')
| -rw-r--r-- | gcc/ada/libgnat/a-textio.ads | 300 |
1 files changed, 142 insertions, 158 deletions
diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads index 9cedab6..ddbbd85 100644 --- a/gcc/ada/libgnat/a-textio.ads +++ b/gcc/ada/libgnat/a-textio.ads @@ -59,7 +59,8 @@ package Ada.Text_IO with SPARK_Mode, Abstract_State => File_System, Initializes => File_System, - Initial_Condition => Line_Length = 0 and Page_Length = 0 + Initial_Condition => Line_Length = 0 and Page_Length = 0, + Always_Terminates is pragma Elaborate_Body; @@ -101,15 +102,15 @@ is Name : String := ""; Form : String := "") with - Pre => not Is_Open (File), - Post => + 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), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Name_Error | Use_Error => Standard.True); procedure Open (File : in out File_Type; @@ -117,57 +118,56 @@ is Name : String; Form : String := "") with - Pre => not Is_Open (File), - Post => + 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), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Name_Error | Use_Error => Standard.True); procedure Close (File : in out File_Type) with - Pre => Is_Open (File), - Post => not Is_Open (File), - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + 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), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File), + Post => not Is_Open (File), + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); procedure Reset (File : in out File_Type; Mode : File_Mode) with - Pre => Is_Open (File), - Post => + 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), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); procedure Reset (File : in out File_Type) with - Pre => Is_Open (File), - Post => + 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), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); 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; + Pre => Is_Open (File), + SPARK_Mode => Off; function Form (File : File_Type) return String with Pre => Is_Open (File), @@ -210,53 +210,51 @@ is -- an oversight, and was intended to be IN, see AI95-00057. procedure Flush (File : File_Type) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + 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), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Flush with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); -------------------------------------------- -- Specification of line and page lengths -- -------------------------------------------- procedure Set_Line_Length (File : File_Type; To : Count) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + 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), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); procedure Set_Line_Length (To : Count) with - Post => + Post => Line_Length = To and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); procedure Set_Page_Length (File : File_Type; To : Count) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + 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), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); procedure Set_Page_Length (To : Count) with - Post => + Post => Page_Length = To and Line_Length'Old = Line_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (Use_Error => Standard.True); function Line_Length (File : File_Type) return Count with Pre => Is_Open (File) and then Mode (File) /= In_File, @@ -277,31 +275,29 @@ is ------------------------------------ procedure New_Line (File : File_Type; Spacing : Positive_Count := 1) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + 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), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure New_Line (Spacing : Positive_Count := 1) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + 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), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Skip_Line (Spacing : Positive_Count := 1) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); function End_Of_Line (File : File_Type) return Boolean with Pre => Is_Open (File) and then Mode (File) = In_File, @@ -311,31 +307,29 @@ is Global => (Input => File_System); procedure New_Page (File : File_Type) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + 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), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure New_Page with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + 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), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Skip_Page with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); function End_Of_Page (File : File_Type) return Boolean with Pre => Is_Open (File) and then Mode (File) = In_File, @@ -352,209 +346,201 @@ is Global => (Input => File_System); procedure Set_Col (File : File_Type; To : Positive_Count) with - Pre => + Pre => Is_Open (File) and then (if Mode (File) /= In_File then (Line_Length (File) = 0 or else To <= Line_Length (File))), - Contract_Cases => + 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), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Set_Col (To : Positive_Count) with - Pre => Line_Length = 0 or To <= Line_Length, - Post => + 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), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Set_Line (File : File_Type; To : Positive_Count) with - Pre => + Pre => Is_Open (File) and then (if Mode (File) /= In_File then (Page_Length (File) = 0 or else To <= Page_Length (File))), - Contract_Cases => + 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), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Set_Line (To : Positive_Count) with - Pre => Page_Length = 0 or To <= Page_Length, - Post => + 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), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); function Col (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System); + SPARK_Mode => Off; function Col return Positive_Count with - Global => (Input => File_System); + SPARK_Mode => Off; function Line (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System); + SPARK_Mode => Off; function Line return Positive_Count with - Global => (Input => File_System); + SPARK_Mode => Off; function Page (File : File_Type) return Positive_Count with - Pre => Is_Open (File), - Global => (Input => File_System); + SPARK_Mode => Off; function Page return Positive_Count with - Global => (Input => File_System); + SPARK_Mode => Off; ---------------------------- -- Character Input-Output -- ---------------------------- procedure Get (File : File_Type; Item : out Character) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Get (Item : out Character) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Put (File : File_Type; Item : Character) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + 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), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Put (Item : Character) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Look_Ahead (File : File_Type; Item : out Character; End_Of_Line : out Boolean) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + 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) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (Input => File_System), - Annotate => (GNATprove, Always_Return); + Global => (Input => File_System); procedure Get_Immediate (File : File_Type; Item : out Character) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Get_Immediate (Item : out Character) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Get_Immediate (File : File_Type; Item : out Character; Available : out Boolean) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); procedure Get_Immediate (Item : out Character; Available : out Boolean) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Standard.True); ------------------------- -- String Input-Output -- ------------------------- procedure Get (File : File_Type; Item : out String) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); procedure Get (Item : out String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); procedure Put (File : File_Type; Item : String) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + 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), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Put (Item : String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Get_Line (File : File_Type; Item : out String; 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), - Annotate => (GNATprove, Might_Not_Return); + 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), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); procedure Get_Line (Item : out String; Last : out Natural) with - Post => + 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), - Annotate => (GNATprove, Might_Not_Return); + Global => (In_Out => File_System), + Exceptional_Cases => (End_Error => Item'Length'Old > 0); function Get_Line (File : File_Type) return String with SPARK_Mode => Off; pragma Ada_05 (Get_Line); @@ -566,21 +552,19 @@ is (File : File_Type; Item : String) with - Pre => Is_Open (File) and then Mode (File) /= In_File, - Post => + 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), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); procedure Put_Line (Item : String) with - Post => + Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, - Global => (In_Out => File_System), - Annotate => (GNATprove, Always_Return); + Global => (In_Out => File_System); --------------------------------------- -- Generic packages for Input-Output -- |