https://gcc.gnu.org/g:6dd2d491e1fb4e7a969c0bbd98b638d7563bc9fb
commit r17-1966-g6dd2d491e1fb4e7a969c0bbd98b638d7563bc9fb Author: Joffrey Huguet <[email protected]> Date: Mon Jun 15 17:40:04 2026 +0200 ada: Fix contracts in Ada.Text_IO This patch adds Data_Error in Exceptional_Cases contracts for Get procedures in Ada.Text_IO. gcc/ada/ChangeLog: * libgnat/a-textio.ads (Get): Add Data_Error in Exceptional_Cases contract. (Look_Ahead): Likewise. (Get_Immediate): Likewise. (Get_Line): Likewise. Diff: --- gcc/ada/libgnat/a-textio.ads | 40 ++++++++++++++++++++++++++-------------- 1 file changed, 26 insertions(+), 14 deletions(-) diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads index 9ba63ddcfa19..5e3504184927 100644 --- a/gcc/ada/libgnat/a-textio.ads +++ b/gcc/ada/libgnat/a-textio.ads @@ -414,14 +414,16 @@ is procedure Get (File : File_Type; Item : out Character) with Pre => Is_Open (File) and then Mode (File) = In_File, Global => (In_Out => File_System), - Exceptional_Cases => (End_Error => Standard.True); + Exceptional_Cases => (End_Error => Standard.True, + Data_Error => Standard.True); procedure Get (Item : out Character) with Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, Global => (In_Out => File_System), - Exceptional_Cases => (End_Error => Standard.True); + Exceptional_Cases => (End_Error => Standard.True, + Data_Error => Standard.True); procedure Put (File : File_Type; Item : Character) with Pre => Is_Open (File) and then Mode (File) /= In_File, @@ -441,17 +443,19 @@ is Item : out Character; End_Of_Line : out Boolean) with - Pre => Is_Open (File) and then Mode (File) = In_File, - Global => (Input => File_System); + Pre => Is_Open (File) and then Mode (File) = In_File, + Global => (Input => File_System), + Exceptional_Cases => (Data_Error => Standard.True); 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); + Global => (Input => File_System), + Exceptional_Cases => (Data_Error => Standard.True); procedure Get_Immediate (File : File_Type; @@ -459,7 +463,8 @@ is with Pre => Is_Open (File) and then Mode (File) = In_File, Global => (In_Out => File_System), - Exceptional_Cases => (End_Error => Standard.True); + Exceptional_Cases => (End_Error => Standard.True, + Data_Error => Standard.True); procedure Get_Immediate (Item : out Character) @@ -468,7 +473,8 @@ is Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, Global => (In_Out => File_System), - Exceptional_Cases => (End_Error => Standard.True); + Exceptional_Cases => (End_Error => Standard.True, + Data_Error => Standard.True); procedure Get_Immediate (File : File_Type; @@ -477,7 +483,8 @@ is with Pre => Is_Open (File) and then Mode (File) = In_File, Global => (In_Out => File_System), - Exceptional_Cases => (End_Error => Standard.True); + Exceptional_Cases => (End_Error => Standard.True, + Data_Error => Standard.True); procedure Get_Immediate (Item : out Character; @@ -487,7 +494,8 @@ is Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, Global => (In_Out => File_System), - Exceptional_Cases => (End_Error => Standard.True); + Exceptional_Cases => (End_Error => Standard.True, + Data_Error => Standard.True); ------------------------- -- String Input-Output -- @@ -496,14 +504,16 @@ is procedure Get (File : File_Type; Item : out String) with Pre => Is_Open (File) and then Mode (File) = In_File, Global => (In_Out => File_System), - Exceptional_Cases => (End_Error => Item'Length'Old > 0); + Exceptional_Cases => (End_Error => Item'Length'Old > 0, + Data_Error => Item'Length'Old > 0); procedure Get (Item : out String) with Post => Line_Length'Old = Line_Length and Page_Length'Old = Page_Length, Global => (In_Out => File_System), - Exceptional_Cases => (End_Error => Item'Length'Old > 0); + Exceptional_Cases => (End_Error => Item'Length'Old > 0, + Data_Error => Item'Length'Old > 0); procedure Put (File : File_Type; Item : String) with Pre => Is_Open (File) and then Mode (File) /= In_File, @@ -530,7 +540,8 @@ is else Last = Item'First - 1) and (for all I in Item'First .. Last => Item (I)'Initialized), Global => (In_Out => File_System), - Exceptional_Cases => (End_Error => Item'Length'Old > 0); + Exceptional_Cases => (End_Error => Item'Length'Old > 0, + Data_Error => Item'Length'Old > 0); procedure Get_Line (Item : out String; @@ -544,7 +555,8 @@ is else Last = Item'First - 1) and (for all I in Item'First .. Last => Item (I)'Initialized), Global => (In_Out => File_System), - Exceptional_Cases => (End_Error => Item'Length'Old > 0); + Exceptional_Cases => (End_Error => Item'Length'Old > 0, + Data_Error => Item'Length'Old > 0); function Get_Line (File : File_Type) return String with SPARK_Mode => Off; pragma Ada_05 (Get_Line);
