From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wm1-x32b.google.com (mail-wm1-x32b.google.com [IPv6:2a00:1450:4864:20::32b]) by sourceware.org (Postfix) with ESMTPS id 4981E3857B9B for ; Tue, 27 Jun 2023 12:08:08 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 4981E3857B9B Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com Received: by mail-wm1-x32b.google.com with SMTP id 5b1f17b1804b1-3fba545d743so6770175e9.0 for ; Tue, 27 Jun 2023 05:08:08 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1687867687; x=1690459687; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=eOcQIaffjY26Xff4mg/wfaofXdXsSCH6n+WP69u44kc=; b=YL9g+h/7ArFOcqkXHjpgTm2JujqmJLSlYFactN+UGBlwW7aqtsRKHKDU3LgPyci9sm 8idsbgdO4HC6VYOnW+39h8V8xmKAOUbkM8COlt/OKXVLf2dj8Y0oC0jLH2JvUYooZSZU q54PTjnedNnaHnFsPJQdaeGQuWI0HEa4YkIxN0w9pytCVjMk25DecMAgRKgImHvHMaU9 41M529DTxmZhOHFZWkC6ZvzpXdWMjoGyEgmdlWfJPLu/SyuXTzHa3MFx+Yp0i671frki pxe2+GIe2Ly9matMfxsbCSXYZseJRH/8M2CWd7944hGwCs6TphnHxsRJ//n5t9/2Hzu8 3BzA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1687867687; x=1690459687; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=eOcQIaffjY26Xff4mg/wfaofXdXsSCH6n+WP69u44kc=; b=Cal1EB7Zu2z+I/6LChQRsV+Ve2r653wM+jcskxo36uz4Iiel1YIgN1MZKqDWIzFQ+T eSEjLdkFFfsyScREs5AO2OXXFHQ9wAzYedd3AbtlrU8NmYnvksLJlhge6z1DAFbIahPp kWzITg1xDdI4CAxXjsw4YWCRZPKRO7sPoANIUYISN+tUeV8npuQcifnt9ZaH8CP/utHx +WxHzaZIasFW4mDuvaLW1gIJt5mfWXuExwsQivfzL9k0cZ1sskEhwTQh7AsWL0Qg7JCN 11zyjpGHJcOoS6OPaNZ3a2AavPkmvrjfSUKBxn64eOYP+dPqZCEIWZ6w2/R5mEiWN4PM 1Qgg== X-Gm-Message-State: AC+VfDxSo3au96I3KyhfZ3Kl7RgLuFtU5+zx3aCeeZHBvxQeE/lMaQCR FqYB1XjJeuIDAZrXEdQn2/B6uCwhB1nd6uRlkBqvnQ== X-Google-Smtp-Source: ACHHUZ77Sau1YU1NAbx7huYEXKZNdizGIFDZ36Tsdw27nnPMizvGVyxZXhZaoTWA95eLyyR5DvjEUg== X-Received: by 2002:a7b:cb99:0:b0:3f9:c9bc:401 with SMTP id m25-20020a7bcb99000000b003f9c9bc0401mr14939892wmi.33.1687867687081; Tue, 27 Jun 2023 05:08:07 -0700 (PDT) Received: from poulhies-Precision-5550.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id y12-20020a05600c364c00b003f7f249e7dfsm13640972wmq.4.2023.06.27.05.08.06 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 27 Jun 2023 05:08:06 -0700 (PDT) From: =?UTF-8?q?Marc=20Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Claire Dross Subject: [COMMITTED] ada: Correct the contract of Ada.Text_IO.Get_Line Date: Tue, 27 Jun 2023 14:08:05 +0200 Message-Id: <20230627120805.3420102-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Status: No, score=-13.7 required=5.0 tests=BAYES_00,DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,GIT_PATCH_0,RCVD_IN_DNSWL_NONE,SPF_HELO_NONE,SPF_PASS,TXREP,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org List-Id: From: Claire Dross 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 --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); -- 2.40.0