[COMMITTED 01/35] ada: Fix docs and comments about pragmas for Boolean-valued aspects

["Marc Poulhiès" <poulhies@adacore.com>]

From: Piotr Trojanek <trojanek@adacore.com>

Fix various inconsistencies in documentation and comments of
Boolean-valued aspects.

gcc/ada/

	* doc/gnat_rm/implementation_defined_pragmas.rst: Fix
	documentation.
	* sem_prag.adb: Fix comments.
	* gnat_rm.texi: Regenerate.

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

---
 .../implementation_defined_pragmas.rst        | 57 +++++++++++--------
 gcc/ada/gnat_rm.texi                          | 57 +++++++++++--------
 gcc/ada/sem_prag.adb                          | 48 ++++++++--------
 3 files changed, 89 insertions(+), 73 deletions(-)

diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
index 3426c34ebe8..7f221e32344 100644
--- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
+++ b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
@@ -341,7 +341,7 @@ Syntax:
   pragma Always_Terminates [ (boolean_EXPRESSION) ];
 
 For the semantics of this pragma, see the entry for aspect ``Always_Terminates``
-in the SPARK 2014 Reference Manual, section 7.1.2.
+in the SPARK 2014 Reference Manual, section 6.1.10.
 
 .. _Pragma-Annotate:
 
@@ -2381,7 +2381,7 @@ Syntax:
 
 .. code-block:: ada
 
-  pragma Favor_Top_Level (type_NAME);
+  pragma Favor_Top_Level (type_LOCAL_NAME);
 
 
 The argument of pragma ``Favor_Top_Level`` must be a named access-to-subprogram
@@ -2838,7 +2838,7 @@ Syntax:
 
 .. code-block:: ada
 
-  pragma Independent (Local_NAME);
+  pragma Independent (component_LOCAL_NAME);
 
 
 This pragma is standard in Ada 2012 mode (which also provides an aspect
@@ -3537,6 +3537,11 @@ Pragma Lock_Free
 ================
 
 Syntax:
+
+.. code-block:: ada
+
+  pragma Lock_Free [ (static_boolean_EXPRESSION) ];
+
 This pragma may be specified for protected types or objects. It specifies that
 the implementation of protected operations must be implemented without locks.
 Compilation fails if the compiler cannot generate lock-free code for the
@@ -3850,7 +3855,7 @@ same name) that establishes the restriction ``No_Elaboration_Code`` for
 the current unit and any extended main source units (body and subunits).
 It also has the effect of enforcing a transitive application of this
 aspect, so that if any unit is implicitly or explicitly with'ed by the
-current unit, it must also have the No_Elaboration_Code_All aspect set.
+current unit, it must also have the `No_Elaboration_Code_All` aspect set.
 It may be applied to package or subprogram specs or their generic versions.
 
 Pragma No_Heap_Finalization
@@ -4508,7 +4513,7 @@ Syntax:
 
 ::
 
-  pragma Persistent_BSS [(LOCAL_NAME)]
+  pragma Persistent_BSS [(object_LOCAL_NAME)]
 
 
 This pragma allows selected objects to be placed in the ``.persistent_bss``
@@ -6500,12 +6505,12 @@ Syntax:
 
 ::
 
-  pragma Suppress_Initialization ([Entity =>] variable_or_subtype_Name);
+  pragma Suppress_Initialization ([Entity =>] variable_or_subtype_LOCAL_NAME);
 
 
-Here variable_or_subtype_Name is the name introduced by a type declaration
-or subtype declaration or the name of a variable introduced by an
-object declaration.
+Here variable_or_subtype_LOCAL_NAME is the name introduced by a type
+declaration or subtype declaration or the name of a variable introduced by
+an object declaration.
 
 In the case of a type or subtype
 this pragma suppresses any implicit or explicit initialization
@@ -6889,22 +6894,24 @@ Syntax:
 
 
 This configuration pragma defines a new aspect, making it available for
-subsequent use in a User_Aspect aspect specification. The first
-identifier is the name of the new aspect. Any subsequent arguments
-specify the names of other aspects. A subsequent name for which no parenthesized
-arguments are given shall denote either a Boolean-valued
-non-representation aspect or an aspect that has been defined by another
-User_Aspect_Definition pragma. A name for which one or more arguments are
-given shall be either Annotate or Local_Restrictions (and the arguments shall
-be appropriate for the named aspect). This pragma, together with the
-User_Aspect aspect, provides a mechanism for
-avoiding textual duplication if some set of aspect specifications is needed
-in multiple places. This is somewhat analogous to how profiles allow avoiding
-duplication of Restrictions pragmas. The visibility rules for an aspect
-defined by a User_Aspect_Definition pragma are the same as for a check name
-introduced by a Check_Name pragma. If multiple
-definitions are visible for some aspect at some point, then the
-definitions must agree. A predefined aspect cannot be redefined.
+subsequent use in a `User_Aspect` aspect specification. The first identifier
+is the name of the new aspect. Any subsequent arguments specify the names
+of other aspects. A subsequent name for which no parenthesized arguments
+are given shall denote either a Boolean-valued non-representation aspect
+or an aspect that has been defined by another `User_Aspect_Definition`
+pragma. A name for which one or more arguments are given shall be either
+`Annotate` or `Local_Restrictions` (and the arguments shall be appropriate
+for the named aspect).
+
+This pragma, together with the `User_Aspect` aspect, provides a mechanism
+for avoiding textual duplication if some set of aspect specifications
+is needed in multiple places. This is somewhat analogous to how profiles
+allow avoiding duplication of `Restrictions` pragmas.
+
+The visibility rules for an aspect defined by a `User_Aspect_Definition`
+pragma are the same as for a check name introduced by a `Check_Name`
+pragma. If multiple definitions are visible for some aspect at some point,
+then the definitions must agree. A predefined aspect cannot be redefined.
 
 
 Pragma Unimplemented_Unit
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index f0e95bec1e5..80de5bb2287 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -1750,7 +1750,7 @@ pragma Always_Terminates [ (boolean_EXPRESSION) ];
 @end example
 
 For the semantics of this pragma, see the entry for aspect @code{Always_Terminates}
-in the SPARK 2014 Reference Manual, section 7.1.2.
+in the SPARK 2014 Reference Manual, section 6.1.10.
 
 @node Pragma Annotate,Pragma Assert,Pragma Always_Terminates,Implementation Defined Pragmas
 @anchor{gnat_rm/implementation_defined_pragmas id4}@anchor{2a}@anchor{gnat_rm/implementation_defined_pragmas pragma-annotate}@anchor{2b}
@@ -3859,7 +3859,7 @@ under control of the pragma, rather than use the preinstantiated versions.
 Syntax:
 
 @example
-pragma Favor_Top_Level (type_NAME);
+pragma Favor_Top_Level (type_LOCAL_NAME);
 @end example
 
 The argument of pragma @code{Favor_Top_Level} must be a named access-to-subprogram
@@ -4319,7 +4319,7 @@ default convention is Ada, which is almost certainly not what is required.
 Syntax:
 
 @example
-pragma Independent (Local_NAME);
+pragma Independent (component_LOCAL_NAME);
 @end example
 
 This pragma is standard in Ada 2012 mode (which also provides an aspect
@@ -5039,6 +5039,11 @@ end IO_Card;
 
 
 Syntax:
+
+@example
+pragma Lock_Free [ (static_boolean_EXPRESSION) ];
+@end example
+
 This pragma may be specified for protected types or objects. It specifies that
 the implementation of protected operations must be implemented without locks.
 Compilation fails if the compiler cannot generate lock-free code for the
@@ -5388,7 +5393,7 @@ same name) that establishes the restriction @code{No_Elaboration_Code} for
 the current unit and any extended main source units (body and subunits).
 It also has the effect of enforcing a transitive application of this
 aspect, so that if any unit is implicitly or explicitly with’ed by the
-current unit, it must also have the No_Elaboration_Code_All aspect set.
+current unit, it must also have the @cite{No_Elaboration_Code_All} aspect set.
 It may be applied to package or subprogram specs or their generic versions.
 
 @node Pragma No_Heap_Finalization,Pragma No_Inline,Pragma No_Elaboration_Code_All,Implementation Defined Pragmas
@@ -6024,7 +6029,7 @@ For more information on the subject of passive tasks, see the section
 Syntax:
 
 @example
-pragma Persistent_BSS [(LOCAL_NAME)]
+pragma Persistent_BSS [(object_LOCAL_NAME)]
 @end example
 
 This pragma allows selected objects to be placed in the @code{.persistent_bss}
@@ -8060,12 +8065,12 @@ with this pragma and others compiled in normal mode without it.
 Syntax:
 
 @example
-pragma Suppress_Initialization ([Entity =>] variable_or_subtype_Name);
+pragma Suppress_Initialization ([Entity =>] variable_or_subtype_LOCAL_NAME);
 @end example
 
-Here variable_or_subtype_Name is the name introduced by a type declaration
-or subtype declaration or the name of a variable introduced by an
-object declaration.
+Here variable_or_subtype_LOCAL_NAME is the name introduced by a type
+declaration or subtype declaration or the name of a variable introduced by
+an object declaration.
 
 In the case of a type or subtype
 this pragma suppresses any implicit or explicit initialization
@@ -8439,22 +8444,24 @@ pragma User_Aspect_Definition
 @end example
 
 This configuration pragma defines a new aspect, making it available for
-subsequent use in a User_Aspect aspect specification. The first
-identifier is the name of the new aspect. Any subsequent arguments
-specify the names of other aspects. A subsequent name for which no parenthesized
-arguments are given shall denote either a Boolean-valued
-non-representation aspect or an aspect that has been defined by another
-User_Aspect_Definition pragma. A name for which one or more arguments are
-given shall be either Annotate or Local_Restrictions (and the arguments shall
-be appropriate for the named aspect). This pragma, together with the
-User_Aspect aspect, provides a mechanism for
-avoiding textual duplication if some set of aspect specifications is needed
-in multiple places. This is somewhat analogous to how profiles allow avoiding
-duplication of Restrictions pragmas. The visibility rules for an aspect
-defined by a User_Aspect_Definition pragma are the same as for a check name
-introduced by a Check_Name pragma. If multiple
-definitions are visible for some aspect at some point, then the
-definitions must agree. A predefined aspect cannot be redefined.
+subsequent use in a @cite{User_Aspect} aspect specification. The first identifier
+is the name of the new aspect. Any subsequent arguments specify the names
+of other aspects. A subsequent name for which no parenthesized arguments
+are given shall denote either a Boolean-valued non-representation aspect
+or an aspect that has been defined by another @cite{User_Aspect_Definition}
+pragma. A name for which one or more arguments are given shall be either
+@cite{Annotate} or @cite{Local_Restrictions} (and the arguments shall be appropriate
+for the named aspect).
+
+This pragma, together with the @cite{User_Aspect} aspect, provides a mechanism
+for avoiding textual duplication if some set of aspect specifications
+is needed in multiple places. This is somewhat analogous to how profiles
+allow avoiding duplication of @cite{Restrictions} pragmas.
+
+The visibility rules for an aspect defined by a @cite{User_Aspect_Definition}
+pragma are the same as for a check name introduced by a @cite{Check_Name}
+pragma. If multiple definitions are visible for some aspect at some point,
+then the definitions must agree. A predefined aspect cannot be redefined.
 
 @node Pragma Unimplemented_Unit,Pragma Universal_Aliasing,Pragma User_Aspect_Definition,Implementation Defined Pragmas
 @anchor{gnat_rm/implementation_defined_pragmas pragma-unimplemented-unit}@anchor{10d}
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 9646e891c46..105cc73eba3 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -13993,11 +13993,11 @@ package body Sem_Prag is
          --                          No_Caching                          --
          ------------------------------------------------------------------
 
-         --  pragma Async_Readers    [ (boolean_EXPRESSION) ];
-         --  pragma Async_Writers    [ (boolean_EXPRESSION) ];
-         --  pragma Effective_Reads  [ (boolean_EXPRESSION) ];
-         --  pragma Effective_Writes [ (boolean_EXPRESSION) ];
-         --  pragma No_Caching       [ (boolean_EXPRESSION) ];
+         --  pragma Async_Readers    [ (static_boolean_EXPRESSION) ];
+         --  pragma Async_Writers    [ (static_boolean_EXPRESSION) ];
+         --  pragma Effective_Reads  [ (static_boolean_EXPRESSION) ];
+         --  pragma Effective_Writes [ (static_boolean_EXPRESSION) ];
+         --  pragma No_Caching       [ (static_boolean_EXPRESSION) ];
 
          when Pragma_Async_Readers
             | Pragma_Async_Writers
@@ -15425,6 +15425,8 @@ package body Sem_Prag is
          -- CUDA_Device --
          -----------------
 
+         --  pragma CUDA_Device (LOCAL_NAME);
+
          when Pragma_CUDA_Device => CUDA_Device : declare
             Arg_Node      : Node_Id;
             Device_Entity : Entity_Id;
@@ -15457,11 +15459,11 @@ package body Sem_Prag is
          -- CUDA_Execute --
          ------------------
 
-         --    pragma CUDA_Execute (PROCEDURE_CALL_STATEMENT,
-         --                         EXPRESSION,
-         --                         EXPRESSION,
-         --                         [, EXPRESSION
-         --                         [, EXPRESSION]]);
+         --  pragma CUDA_Execute (PROCEDURE_CALL_STATEMENT,
+         --                       EXPRESSION,
+         --                       EXPRESSION,
+         --                       [, EXPRESSION
+         --                       [, EXPRESSION]]);
 
          when Pragma_CUDA_Execute => CUDA_Execute : declare
 
@@ -15556,7 +15558,7 @@ package body Sem_Prag is
          -- CUDA_Global --
          -----------------
 
-         --  pragma CUDA_Global ([Entity =>] IDENTIFIER);
+         --  pragma CUDA_Global ([Entity =>] procedure_LOCAL_NAME);
 
          when Pragma_CUDA_Global => CUDA_Global : declare
             Arg_Node    : Node_Id;
@@ -17326,7 +17328,7 @@ package body Sem_Prag is
          -- Extensions_Visible --
          ------------------------
 
-         --  pragma Extensions_Visible [ (boolean_EXPRESSION) ];
+         --  pragma Extensions_Visible [ (static_boolean_EXPRESSION) ];
 
          --  Characteristics:
 
@@ -17565,7 +17567,7 @@ package body Sem_Prag is
          -- Favor_Top_Level --
          --------------------------
 
-         --  pragma Favor_Top_Level (type_NAME);
+         --  pragma Favor_Top_Level (type_LOCAL_NAME);
 
          when Pragma_Favor_Top_Level => Favor_Top_Level : declare
             Typ : Entity_Id;
@@ -17643,7 +17645,7 @@ package body Sem_Prag is
          -- Ghost --
          -----------
 
-         --  pragma Ghost [ (boolean_EXPRESSION) ];
+         --  pragma Ghost [ (static_boolean_EXPRESSION) ];
 
          when Pragma_Ghost => Ghost : declare
             Context   : Node_Id;
@@ -19668,8 +19670,8 @@ package body Sem_Prag is
          ------------------
 
          --  pragma Linker_Alias (
-         --      [Entity =>]  LOCAL_NAME
-         --      [Target =>]  static_string_EXPRESSION);
+         --      [Entity =>] LOCAL_NAME
+         --      [Target =>] static_string_EXPRESSION);
 
          when Pragma_Linker_Alias =>
             GNAT_Pragma;
@@ -19940,7 +19942,7 @@ package body Sem_Prag is
          -- Lock_Free --
          ---------------
 
-         --  pragma Lock_Free [(Boolean_EXPRESSION)];
+         --  pragma Lock_Free [(static_boolean_EXPRESSION)];
 
          when Pragma_Lock_Free => Lock_Free : declare
             P   : constant Node_Id := Parent (N);
@@ -20685,7 +20687,7 @@ package body Sem_Prag is
          -- No_Return --
          ---------------
 
-         --  pragma No_Return (procedure_LOCAL_NAME {, procedure_Local_Name});
+         --  pragma No_Return (procedure_LOCAL_NAME {, procedure_LOCAL_NAME});
 
          when Pragma_No_Return => Prag_No_Return : declare
 
@@ -21971,7 +21973,7 @@ package body Sem_Prag is
          -- Persistent_BSS --
          --------------------
 
-         --  pragma Persistent_BSS [(object_NAME)];
+         --  pragma Persistent_BSS [(object_LOCAL_NAME)];
 
          when Pragma_Persistent_BSS => Persistent_BSS :  declare
             Decl : Node_Id;
@@ -25318,7 +25320,7 @@ package body Sem_Prag is
          -- Suppress_Initialization --
          -----------------------------
 
-         --  pragma Suppress_Initialization ([Entity =>] type_Name);
+         --  pragma Suppress_Initialization ([Entity =>] type_LOCAL_NAME);
 
          when Pragma_Suppress_Initialization => Suppress_Init : declare
             E    : Entity_Id;
@@ -25945,7 +25947,7 @@ package body Sem_Prag is
          -- Unchecked_Union --
          ---------------------
 
-         --  pragma Unchecked_Union (first_subtype_LOCAL_NAME)
+         --  pragma Unchecked_Union (first_subtype_LOCAL_NAME);
 
          when Pragma_Unchecked_Union => Unchecked_Union : declare
             Assoc   : constant Node_Id := Arg1;
@@ -26155,7 +26157,7 @@ package body Sem_Prag is
 
          --    or when used in a context clause:
 
-         --  pragma Unreferenced (library_unit_NAME {, library_unit_NAME}
+         --  pragma Unreferenced (library_unit_NAME {, library_unit_NAME});
 
          when Pragma_Unreferenced =>
             Analyze_Unreferenced_Or_Unused;
@@ -26563,7 +26565,7 @@ package body Sem_Prag is
          -- Volatile_Function --
          -----------------------
 
-         --  pragma Volatile_Function [ (boolean_EXPRESSION) ];
+         --  pragma Volatile_Function [ (static_boolean_EXPRESSION) ];
 
          when Pragma_Volatile_Function => Volatile_Function : declare
             Over_Id   : Entity_Id;
-- 
2.43.2