diff mbox series

[COMMITTED] ada: Correct the contract of Ada.Text_IO.Get_Line

Message ID 20230627120805.3420102-1-poulhies@adacore.com
State Unresolved
Headers
Series [COMMITTED] ada: Correct the contract of Ada.Text_IO.Get_Line |

Checks

Context Check Description
snail/gcc-patch-check warning Git am fail log

Commit Message

Marc Poulhiès June 27, 2023, 12:08 p.m. UTC 
  From: Claire Dross <dross@adacore.com>

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.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/a-textio.ads | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)
diff mbox series

Patch

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);