From: Piotr Trojanek <troja...@adacore.com>
Add description of a recently added SPARK contract.
gcc/ada/
* doc/gnat_rm/implementation_defined_aspects.rst,
doc/gnat_rm/implementation_defined_pragmas.rst: Add sections for
Always_Terminates.
* gnat-style.texi: Regenerate.
* gnat_rm.texi: Regenerate.
* gnat_ugn.texi: Regenerate.
---
.../doc/gnat_rm/implementation_defined_aspects.rst | 6 ++++++
.../doc/gnat_rm/implementation_defined_pragmas.rst | 14 ++++++++++++++
2 files changed, 20 insertions(+)
diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst
b/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst
index 3d90ad5b210..d58119b5fbc 100644
--- a/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst
+++ b/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst
@@ -66,6 +66,12 @@ Aspect Abstract_State
This aspect is equivalent to :ref:`pragma
Abstract_State<Pragma-Abstract_State>`.
+Aspect Always_Terminates
+========================
+.. index:: Always_Terminates
+
+This boolean aspect is equivalent to :ref:`pragma
Always_Terminates<Pragma-Always_Terminates>`.
+
Aspect Annotate
===============
diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
index bfaa1cff407..9fc334354ac 100644
--- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
+++ b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
@@ -329,6 +329,20 @@ this pragma serves no purpose but is ignored
rather than rejected to allow common sets of sources to be used
in the two situations.
+.. _Pragma-Always_Terminates:
+
+Pragma Always_Terminates
+========================
+
+Syntax:
+
+.. code-block:: ada
+
+ 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.
+
.. _Pragma-Annotate:
Pragma Annotate
--
2.43.0
