@@ -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
===============
@@ -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
From: Piotr Trojanek <trojanek@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(+)