diff mbox series

[COMMITTED] ada: Document new SPARK aspect and pragma Always_Terminates

Message ID 20240109133640.752216-1-poulhies@adacore.com
State Accepted
Headers
Series [COMMITTED] ada: Document new SPARK aspect and pragma Always_Terminates |

Checks

Context Check Description
snail/gcc-patch-check success Github commit url

Commit Message

Marc Poulhiès Jan. 9, 2024, 1:36 p.m. UTC 
  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(+)
diff mbox series

Patch

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