From: Claire Dross <dross@adacore.com>
Date: Wed, 14 Jun 2023 11:05:12 +0000 (+0200)
Subject: ada: Correct the contract of Ada.Text_IO.Get_Line
X-Git-Tag: basepoints/gcc-15~8012
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=cba529bc70be52bbc7796faea212fb694d2d25a4;p=thirdparty%2Fgcc.git

ada: Correct the contract of Ada.Text_IO.Get_Line

Item might not be entirely initialized after a call to Get_Line.

gcc/ada/

	* libgnat/a-textio.ads (Get_Line): Use Relaxed_Initialization on
	the Item parameter of Get_Line.
---

diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads
index ddbbd8592ccf..4318b6c62b8f 100644
--- a/gcc/ada/libgnat/a-textio.ads
+++ b/gcc/ada/libgnat/a-textio.ads
@@ -523,24 +523,28 @@ is
       Item : out String;
       Last : out Natural)
    with
-     Pre               => Is_Open (File) and then Mode (File) = In_File,
-     Post              =>
+     Relaxed_Initialization => Item,
+     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);
+        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);
 
    procedure Get_Line
      (Item : out String;
       Last : out Natural)
    with
-     Post              =>
+     Relaxed_Initialization => Item,
+     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),
-     Exceptional_Cases => (End_Error => Item'Length'Old > 0);
+            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);
 
    function Get_Line (File : File_Type) return String with SPARK_Mode => Off;
    pragma Ada_05 (Get_Line);