From patchwork Tue May 17 08:27:29 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 1632111 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: bilbo.ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.a=rsa-sha256 header.s=default header.b=mMGmVxb6; dkim-atps=neutral Authentication-Results: ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=8.43.85.97; helo=sourceware.org; envelope-from=gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Received: from sourceware.org (ip-8-43-85-97.sourceware.org [8.43.85.97]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by bilbo.ozlabs.org (Postfix) with ESMTPS id 4L2TqS4HW7z9s0r for ; Tue, 17 May 2022 18:31:31 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id ED8453857430 for ; Tue, 17 May 2022 08:31:29 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org ED8453857430 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1652776290; bh=1nriR5SQ4DBXJgmACiMWhR1w8IuhdNCApwFMZB2726M=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=mMGmVxb6yWXqgWKkSieLiu/Ay8bejqp7pK7cEn/9lB/gieNroAd0EZNauQwqllawz MaSzaQJyW8MyKPukHX2AAiPMVNCjJ/ew3zLonL0vT8lpo0Pks/aEUm+SIzkmHJK8Bq KO2Sh5PiONxecRRWQIoMRWeOSteMIIMl9THlLV5w= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x32e.google.com (mail-wm1-x32e.google.com [IPv6:2a00:1450:4864:20::32e]) by sourceware.org (Postfix) with ESMTPS id A3C1C3857419 for ; Tue, 17 May 2022 08:27:31 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org A3C1C3857419 Received: by mail-wm1-x32e.google.com with SMTP id bd25-20020a05600c1f1900b0039485220e16so924291wmb.0 for ; Tue, 17 May 2022 01:27:31 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=1nriR5SQ4DBXJgmACiMWhR1w8IuhdNCApwFMZB2726M=; b=n0JJ1hb3V6NJUG72HT3Vc5Fx6Le17QdWSmIaCYJKu0UBgf3LuyJArLWwXGyeMEKDT6 626+WKJ1By0W+TIViJlFa44HIEJheGpUXkpuYQ4tJh7fyoLl/R3OVNxnAtSxK2t/9oJP 5wlOubsOCu3LaD2d5xFO7yFnhSwNlOfWl7Rslfpv/427nfi5leoIFmyfHaSzmkukMDLy xMIYYiLo3Bnh/oW+UXRZ7jF0sW3guiK3CxQqjePbsX88s/xHbTU8IQRYlHODosStMqJB ax0ZqNbQwaJ/+wPTYiCkXULZkBn8fyTw2gMcU1bnihit39LeKMMRCugUleLSdZho82Q+ yeCA== X-Gm-Message-State: AOAM530NE6Wc03mhFmGqiq3nbZWSjt17L09Ras3S8WGseQ5CvbcSoN/F SZKpMBS5NTdWGYpv1gurGLtXdYq9FNn7BIjr X-Google-Smtp-Source: ABdhPJzRn7ucsIbDM8+0QjbiCb4CRyKpvUEMadV3HdKEQVhGjHEVKl59btPT+FJXvi7nx3HV9qxQxw== X-Received: by 2002:a05:600c:3595:b0:394:8343:a66d with SMTP id p21-20020a05600c359500b003948343a66dmr31052226wmq.49.1652776050440; Tue, 17 May 2022 01:27:30 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id m13-20020a7bcf2d000000b003942a244f47sm1218257wmg.32.2022.05.17.01.27.29 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 17 May 2022 01:27:29 -0700 (PDT) Date: Tue, 17 May 2022 08:27:29 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Fix documentation of using attribute Loop_Entry in pragmas Message-ID: <20220517082729.GA1087596@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-13.2 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: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Piotr Trojanek Errors-To: gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org Sender: "Gcc-patches" Attribute Loop_Entry was initially only allowed to appear in pragmas Loop_Variant and Loop_Invariant. Then it was also allowed to appear in pragmas Assert, Assert_And_Cut and Assume, but this change was not reflected in the GNAT RM. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * doc/gnat_rm/implementation_defined_attributes.rst (Loop_Entry): Mention pragmas Assert, Assert_And_Cut and Assume; refill. * gnat_rm.texi: Regenerate. diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_attributes.rst b/gcc/ada/doc/gnat_rm/implementation_defined_attributes.rst --- a/gcc/ada/doc/gnat_rm/implementation_defined_attributes.rst +++ b/gcc/ada/doc/gnat_rm/implementation_defined_attributes.rst @@ -629,10 +629,13 @@ to the value an expression had upon entry to the subprogram. The relevant loop is either identified by the given loop name, or it is the innermost enclosing loop when no loop name is given. -A ``Loop_Entry`` attribute can only occur within a -``Loop_Variant`` or ``Loop_Invariant`` pragma. A common use of -``Loop_Entry`` is to compare the current value of objects with their -initial value at loop entry, in a ``Loop_Invariant`` pragma. +A ``Loop_Entry`` attribute can only occur within an ``Assert``, +``Assert_And_Cut``, ``Assume``, ``Loop_Variant`` or ``Loop_Invariant`` pragma. +In addition, such a pragma must be one of the items in the sequence +of statements of a loop body, or nested inside block statements that +appear in the sequence of statements of a loop body. +A common use of ``Loop_Entry`` is to compare the current value of objects with +their initial value at loop entry, in a ``Loop_Invariant`` pragma. The effect of using ``X'Loop_Entry`` is the same as declaring a constant initialized with the initial value of ``X`` at loop diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -11028,10 +11028,13 @@ to the value an expression had upon entry to the subprogram. The relevant loop is either identified by the given loop name, or it is the innermost enclosing loop when no loop name is given. -A @code{Loop_Entry} attribute can only occur within a -@code{Loop_Variant} or @code{Loop_Invariant} pragma. A common use of -@code{Loop_Entry} is to compare the current value of objects with their -initial value at loop entry, in a @code{Loop_Invariant} pragma. +A @code{Loop_Entry} attribute can only occur within an @code{Assert}, +@code{Assert_And_Cut}, @code{Assume}, @code{Loop_Variant} or @code{Loop_Invariant} pragma. +In addition, such a pragma must be one of the items in the sequence +of statements of a loop body, or nested inside block statements that +appear in the sequence of statements of a loop body. +A common use of @code{Loop_Entry} is to compare the current value of objects with +their initial value at loop entry, in a @code{Loop_Invariant} pragma. The effect of using @code{X'Loop_Entry} is the same as declaring a constant initialized with the initial value of @code{X} at loop