From patchwork Tue Jun 27 12:08:05 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 113385 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:994d:0:b0:3d9:f83d:47d9 with SMTP id k13csp8144566vqr; Tue, 27 Jun 2023 05:10:05 -0700 (PDT) X-Google-Smtp-Source: ACHHUZ4m6PylP3m2w27tv3rQMu0ibK5wfVvFjOIA+yVlAza7E4Hcf6obfFdUvvXWDb2EVPnDRxBF X-Received: by 2002:a05:6512:23a5:b0:4fb:780c:fce9 with SMTP id c37-20020a05651223a500b004fb780cfce9mr4116668lfv.58.1687867805538; Tue, 27 Jun 2023 05:10:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1687867805; cv=none; d=google.com; s=arc-20160816; b=FHcNPfWCmTuZMvPrLg5MpQOkXj5Dmml+0SR4zDKmo/CVzlmpPG5N+rAIFucIFrOZpg SZnmoLIVLvhnSJHKhis3CFjG5sAuWLcnGqsHYXHjdzra0wIOu0vIIaV5Mh1EoqLedd3E fgBfleiyrUpNK912LOUYhRCChzWRj9m7jbvzGVhbvBlLVB1l/Mn5lvZMZ9pYfYbohDw5 IWzJAPaso8mmcXs08jtuKgB26OcmbDQfIZPnFWKQI2rToUWwA6jEoYK9f189viNxkFUN o6bOyXSWBu3u8phlqhLKf5Jc5dLUzvhSR/hFkWKstGvJEmj5MbdQtQSCuSNJy4A6MuDx fcWQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:reply-to:from:list-subscribe:list-help:list-post :list-archive:list-unsubscribe:list-id:precedence :content-transfer-encoding:mime-version:message-id:date:subject:cc :to:dmarc-filter:delivered-to:dkim-signature:dkim-filter; bh=eOcQIaffjY26Xff4mg/wfaofXdXsSCH6n+WP69u44kc=; fh=jUVcu7GiFfyFz7IG8NRPradprPQUTTD5s1Bm7R/Im+I=; b=MKTGdm5I6sOjReosnri2+FKc5sJceWTQTp7TuZSRTLw0kSJTHHotMJK3jA3A+hEO6z Or26VgW7+OmMkJnc30oApH+AnYioYUsVgVZsxFY61/OcDAKu0b6zkYNujUAo9MfDV+Ke qxNjlNYhYXsSSMNwQ03UmNF+JX1rfAMv7DwgzpkPANacRRWYSXoRDQTsiZRNDPBOGXg1 k2bUgW/rlgkyORcpVXBNTaButDdSg9qHxoJnxIQhaJvmHo0ji2qchTKqggrMcDjyja7L Ks6QQPZ840S2XbTd7bQE55kYx7IULK6osxyvzk9g209yGtdsgFipdfp9YHEXPLavMtxO Xa5A== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=GIJ6ZD4C; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from sourceware.org (server2.sourceware.org. [2620:52:3:1:0:246e:9693:128c]) by mx.google.com with ESMTPS id z13-20020aa7d40d000000b0051daf2b4594si394081edq.447.2023.06.27.05.10.04 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 27 Jun 2023 05:10:05 -0700 (PDT) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) client-ip=2620:52:3:1:0:246e:9693:128c; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=GIJ6ZD4C; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id A0F4E384A86C for ; Tue, 27 Jun 2023 12:08:59 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org A0F4E384A86C DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1687867739; bh=eOcQIaffjY26Xff4mg/wfaofXdXsSCH6n+WP69u44kc=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=GIJ6ZD4CWJp+QEsJB704NWhWT9t/Ed7wg+OXQ6WTnh1C6m5pzRDyNEx2RgWyb/UeQ aOyyv85Ufoo72aSheHy+r1ac2U85fVIkxfavgbcyaq47WKxwEy6Gk3LuDVXybZAndJ 491C+YznG5c6oj0UrnY67Te7yJdWeeXw4lgi+sqg= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org 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 Received: by mail-wm1-x32b.google.com with SMTP id 5b1f17b1804b1-3fba545d743so6770175e9.0 for ; Tue, 27 Jun 2023 05:08:08 -0700 (PDT) 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-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) 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 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 X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: =?utf-8?q?Marc_Poulhi=C3=A8s_via_Gcc-patches?= From: =?utf-8?q?Marc_Poulhi=C3=A8s?= Reply-To: =?utf-8?q?Marc_Poulhi=C3=A8s?= Errors-To: gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org Sender: "Gcc-patches" X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1769857672181792737?= X-GMAIL-MSGID: =?utf-8?q?1769857672181792737?= 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);