diff mbox series

[Ada] Fix documentation of using attribute Loop_Entry in pragmas

Message ID 20220517082729.GA1087596@adacore.com
State New
Headers show
Series [Ada] Fix documentation of using attribute Loop_Entry in pragmas | expand

Commit Message

Pierre-Marie de Rodat May 17, 2022, 8:27 a.m. UTC 
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 mbox series

Patch

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