[gcc r14-2127] ada: Correct the contract of Ada.Text_IO.Get_Line

[gcc r14-2127] ada: Correct the contract of Ada.Text_IO.Get_Line

[Marc Poulhi?s]

https://gcc.gnu.org/g:cba529bc70be52bbc7796faea212fb694d2d25a4

commit r14-2127-gcba529bc70be52bbc7796faea212fb694d2d25a4
Author: Claire Dross <dross@adacore.com>
Date:   Wed Jun 14 13:05:12 2023 +0200

    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:
---
 gcc/ada/libgnat/a-textio.ads | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads
index ddbbd8592cc..4318b6c62b8 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);