diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2024-05-16 22:13:38 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2024-06-20 10:50:54 +0200 |
| commit | 7e057326a901155bccc0ae559191220144a4f6b9 (patch) | |
| tree | cac6ff3315fe57e0362c1532147afbc90c8a46b9 /gcc/ada/doc/gnat_rm | |
| parent | 4f6ee98c27cf0219779a2ccd6ef5d0e67b75580f (diff) | |
| download | gcc-7e057326a901155bccc0ae559191220144a4f6b9.zip gcc-7e057326a901155bccc0ae559191220144a4f6b9.tar.gz gcc-7e057326a901155bccc0ae559191220144a4f6b9.tar.bz2 | |
ada: Add documentation for Subprogram_Variant aspect and pragma
For completeness, the GNAT Reference Manual should document aspects and
pragmas that are specific to SPARK and described in the SPARK User's
Guide.
gcc/ada/
* doc/gnat_rm/implementation_defined_aspects.rst
(Aspect Subprogram_Variant): Refer to SPARK User's Guide.
* doc/gnat_rm/implementation_defined_pragmas.rst
(Pragma Subprogram_Variant): Document syntax to satisfy the
convention; refer to SPARK User's Guide for semantics.
* gnat_rm.texi: Regenerate.
* gnat_ugn.texi: Regenerate.
Diffstat (limited to 'gcc/ada/doc/gnat_rm')
| -rw-r--r-- | gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst | 7 | ||||
| -rw-r--r-- | gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst | 30 |
2 files changed, 37 insertions, 0 deletions
diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst b/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst index ec09fe7..e19684c 100644 --- a/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst +++ b/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst @@ -620,6 +620,13 @@ This aspect is equivalent to :ref:`pragma SPARK_Mode<Pragma-SPARK_Mode>` and may be specified for either or both of the specification and body of a subprogram or package. +Aspect Subprogram_Variant +========================= +.. index:: Subprogram_Variant + +For the syntax and semantics of this aspect, see the SPARK 2014 Reference +Manual, section 6.1.8. + Aspect Suppress_Debug_Info ========================== .. index:: Suppress_Debug_Info diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst index 0661670..acfa729 100644 --- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst +++ b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst @@ -6347,6 +6347,36 @@ for the specified entity, as shown in the following example: pragma Style_Checks (Off, Arg); Rf2 : Integer := ARG; -- OK, no error +Pragma Subprogram_Variant +========================= +.. index:: Subprogram_Variant + +Syntax: + + +:: + + pragma Subprogram_Variant (SUBPROGRAM_VARIANT_LIST); + + SUBPROGRAM_VARIANT_LIST ::= + STRUCTURAL_SUBPROGRAM_VARIANT_ITEM + | NUMERIC_SUBPROGRAM_VARIANT_ITEMS + + NUMERIC_SUBPROGRAM_VARIANT_ITEMS ::= + NUMERIC_SUBPROGRAM_VARIANT_ITEM {, NUMERIC_SUBPROGRAM_VARIANT_ITEM} + + NUMERIC_SUBPROGRAM_VARIANT_ITEM ::= + CHANGE_DIRECTION => EXPRESSION + + STRUCTURAL_SUBPROGRAM_VARIANT_ITEM ::= + STRUCTURAL => EXPRESSION + + CHANGE_DIRECTION ::= Increases | Decreases + +The ``Subprogram_Variant`` pragma is intended to be an exact replacement for +the implementation-defined ``Subprogram_Variant`` aspect, and shares its +restrictions and semantics. + Pragma Subtitle =============== |