ada: Document new SPARK aspect and pragma Always_Terminates

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.

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
 ===============
 

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

gcc/ada/gnat-style.texi

@@ -3,7 +3,7 @@
 @setfilename gnat-style.info
 @documentencoding UTF-8
 @ifinfo
-@*Generated by Sphinx 4.3.2.@*
+@*Generated by Sphinx 5.3.0.@*
 @end ifinfo
 @settitle GNAT Coding Style A Guide for GNAT Developers
 @defindex ge
@@ -15,13 +15,11 @@
 * gnat-style: (gnat-style.info). gnat-style
 @end direntry
 
-@definfoenclose strong,`,'
-@definfoenclose emph,`,'
 @c %**end of header
 
 @copying
 @quotation
-GNAT Coding Style: A Guide for GNAT Developers , Dec 14, 2023
+GNAT Coding Style: A Guide for GNAT Developers , Dec 21, 2023
 
 AdaCore
 
@@ -255,7 +253,7 @@ When declarations are commented with ‘hanging’ comments, i.e.
 comments after the declaration, there is no blank line before the
 comment, and if it is absolutely necessary to have blank lines within
 the comments, e.g. to make paragraph separations within a single comment,
-these blank lines @emph{do} have a @code{--} (unlike the
+these blank lines `do' have a @code{--} (unlike the
 normal rule, which is to use entirely blank lines for separating
 comment paragraphs).  The comment starts at same level of indentation
 as code it is commenting.
@@ -304,12 +302,12 @@ Other_Id := 6;           --  Second comment
 @end example
 
 @item 
-Short comments that fit on a single line are @emph{not} ended with a
+Short comments that fit on a single line are `not' ended with a
 period.  Comments taking more than a line are punctuated in the normal
 manner.
 
 @item 
-Comments should focus on @emph{why} instead of @emph{what}.
+Comments should focus on `why' instead of `what'.
 Descriptions of what subprograms do go with the specification.
 
 @item 
@@ -319,7 +317,7 @@ depend on the names of things.  The names are supplementary, not
 sufficient, as comments.
 
 @item 
-@emph{Do not} put two spaces after periods in comments.
+`Do not' put two spaces after periods in comments.
 @end itemize
 
 @node Declarations and Types,Expressions and Names,Lexical Elements,Top
@@ -958,7 +956,7 @@ Copyright  2000, 2001, 2002, 2007, 2008  Free Software Foundation, Inc
 Everyone is permitted to copy and distribute verbatim copies of this
 license document, but changing it is not allowed.
 
-@strong{Preamble}
+`Preamble'
 
 The purpose of this License is to make a manual, textbook, or other
 functional and useful document “free” in the sense of freedom: to
@@ -981,23 +979,23 @@ it can be used for any textual work, regardless of subject matter or
 whether it is published as a printed book.  We recommend this License
 principally for works whose purpose is instruction or reference.
 
-@strong{1. APPLICABILITY AND DEFINITIONS}
+`1. APPLICABILITY AND DEFINITIONS'
 
 This License applies to any manual or other work, in any medium, that
 contains a notice placed by the copyright holder saying it can be
 distributed under the terms of this License.  Such a notice grants a
 world-wide, royalty-free license, unlimited in duration, to use that
-work under the conditions stated herein.  The @strong{Document}, below,
+work under the conditions stated herein.  The `Document', below,
 refers to any such manual or work.  Any member of the public is a
-licensee, and is addressed as “@strong{you}”.  You accept the license if you
+licensee, and is addressed as “`you'”.  You accept the license if you
 copy, modify or distribute the work in a way requiring permission
 under copyright law.
 
-A “@strong{Modified Version}” of the Document means any work containing the
+A “`Modified Version'” of the Document means any work containing the
 Document or a portion of it, either copied verbatim, or with
 modifications and/or translated into another language.
 
-A “@strong{Secondary Section}” is a named appendix or a front-matter section of
+A “`Secondary Section'” is a named appendix or a front-matter section of
 the Document that deals exclusively with the relationship of the
 publishers or authors of the Document to the Document’s overall subject
 (or to related matters) and contains nothing that could fall directly
@@ -1008,7 +1006,7 @@ connection with the subject or with related matters, or of legal,
 commercial, philosophical, ethical or political position regarding
 them.
 
-The “@strong{Invariant Sections}” are certain Secondary Sections whose titles
+The “`Invariant Sections'” are certain Secondary Sections whose titles
 are designated, as being those of Invariant Sections, in the notice
 that says that the Document is released under this License.  If a
 section does not fit the above definition of Secondary then it is not
@@ -1016,12 +1014,12 @@ allowed to be designated as Invariant.  The Document may contain zero
 Invariant Sections.  If the Document does not identify any Invariant
 Sections then there are none.
 
-The “@strong{Cover Texts}” are certain short passages of text that are listed,
+The “`Cover Texts'” are certain short passages of text that are listed,
 as Front-Cover Texts or Back-Cover Texts, in the notice that says that
 the Document is released under this License.  A Front-Cover Text may
 be at most 5 words, and a Back-Cover Text may be at most 25 words.
 
-A “@strong{Transparent}” copy of the Document means a machine-readable copy,
+A “`Transparent'” copy of the Document means a machine-readable copy,
 represented in a format whose specification is available to the
 general public, that is suitable for revising the document
 straightforwardly with generic text editors or (for images composed of
@@ -1032,7 +1030,7 @@ to text formatters.  A copy made in an otherwise Transparent file
 format whose markup, or absence of markup, has been arranged to thwart
 or discourage subsequent modification by readers is not Transparent.
 An image format is not Transparent if used for any substantial amount
-of text.  A copy that is not “Transparent” is called @strong{Opaque}.
+of text.  A copy that is not “Transparent” is called `Opaque'.
 
 Examples of suitable formats for Transparent copies include plain
 ASCII without markup, Texinfo input format, LaTeX input format, SGML
@@ -1045,22 +1043,22 @@ processing tools are not generally available, and the
 machine-generated HTML, PostScript or PDF produced by some word
 processors for output purposes only.
 
-The “@strong{Title Page}” means, for a printed book, the title page itself,
+The “`Title Page'” means, for a printed book, the title page itself,
 plus such following pages as are needed to hold, legibly, the material
 this License requires to appear in the title page.  For works in
 formats which do not have any title page as such, “Title Page” means
 the text near the most prominent appearance of the work’s title,
 preceding the beginning of the body of the text.
 
-The “@strong{publisher}” means any person or entity that distributes
+The “`publisher'” means any person or entity that distributes
 copies of the Document to the public.
 
-A section “@strong{Entitled XYZ}” means a named subunit of the Document whose
+A section “`Entitled XYZ'” means a named subunit of the Document whose
 title either is precisely XYZ or contains XYZ in parentheses following
 text that translates XYZ in another language.  (Here XYZ stands for a
-specific section name mentioned below, such as “@strong{Acknowledgements}”,
-“@strong{Dedications}”, “@strong{Endorsements}”, or “@strong{History}”.)
-To “@strong{Preserve the Title}”
+specific section name mentioned below, such as “`Acknowledgements'”,
+“`Dedications'”, “`Endorsements'”, or “`History'”.)
+To “`Preserve the Title'”
 of such a section when you modify the Document means that it remains a
 section “Entitled XYZ” according to this definition.
 
@@ -1071,7 +1069,7 @@ License, but only as regards disclaiming warranties: any other
 implication that these Warranty Disclaimers may have is void and has
 no effect on the meaning of this License.
 
-@strong{2. VERBATIM COPYING}
+`2. VERBATIM COPYING'
 
 You may copy and distribute the Document in any medium, either
 commercially or noncommercially, provided that this License, the
@@ -1086,7 +1084,7 @@ number of copies you must also follow the conditions in section 3.
 You may also lend copies, under the same conditions stated above, and
 you may publicly display copies.
 
-@strong{3. COPYING IN QUANTITY}
+`3. COPYING IN QUANTITY'
 
 If you publish printed copies (or copies in media that commonly have
 printed covers) of the Document, numbering more than 100, and the
@@ -1123,7 +1121,7 @@ It is requested, but not required, that you contact the authors of the
 Document well before redistributing any large number of copies, to give
 them a chance to provide you with an updated version of the Document.
 
-@strong{4. MODIFICATIONS}
+`4. MODIFICATIONS'
 
 You may copy and distribute a Modified Version of the Document under
 the conditions of sections 2 and 3 above, provided that you release
@@ -1240,7 +1238,7 @@ The author(s) and publisher(s) of the Document do not by this License
 give permission to use their names for publicity for or to assert or
 imply endorsement of any Modified Version.
 
-@strong{5. COMBINING DOCUMENTS}
+`5. COMBINING DOCUMENTS'
 
 You may combine the Document with other documents released under this
 License, under the terms defined in section 4 above for modified
@@ -1264,7 +1262,7 @@ in the various original documents, forming one section Entitled
 and any sections Entitled “Dedications”.  You must delete all sections
 Entitled “Endorsements”.
 
-@strong{6. COLLECTIONS OF DOCUMENTS}
+`6. COLLECTIONS OF DOCUMENTS'
 
 You may make a collection consisting of the Document and other documents
 released under this License, and replace the individual copies of this
@@ -1277,7 +1275,7 @@ it individually under this License, provided you insert a copy of this
 License into the extracted document, and follow this License in all
 other respects regarding verbatim copying of that document.
 
-@strong{7. AGGREGATION WITH INDEPENDENT WORKS}
+`7. AGGREGATION WITH INDEPENDENT WORKS'
 
 A compilation of the Document or its derivatives with other separate
 and independent documents or works, in or on a volume of a storage or
@@ -1296,7 +1294,7 @@ electronic equivalent of covers if the Document is in electronic form.
 Otherwise they must appear on printed covers that bracket the whole
 aggregate.
 
-@strong{8. TRANSLATION}
+`8. TRANSLATION'
 
 Translation is considered a kind of modification, so you may
 distribute translations of the Document under the terms of section 4.
@@ -1316,7 +1314,7 @@ If a section in the Document is Entitled “Acknowledgements”,
 its Title (section 1) will typically require changing the actual
 title.
 
-@strong{9. TERMINATION}
+`9. TERMINATION'
 
 You may not copy, modify, sublicense, or distribute the Document
 except as expressly provided under this License.  Any attempt
@@ -1343,7 +1341,7 @@ this License.  If your rights have been terminated and not permanently
 reinstated, receipt of a copy of some or all of the same material does
 not give you any rights to use it.
 
-@strong{10. FUTURE REVISIONS OF THIS LICENSE}
+`10. FUTURE REVISIONS OF THIS LICENSE'
 
 The Free Software Foundation may publish new, revised versions
 of the GNU Free Documentation License from time to time.  Such new
@@ -1364,7 +1362,7 @@ License can be used, that proxy’s public statement of acceptance of a
 version permanently authorizes you to choose that version for the
 Document.
 
-@strong{11. RELICENSING}
+`11. RELICENSING'
 
 “Massive Multiauthor Collaboration Site” (or “MMC Site”) means any
 World Wide Web server that publishes copyrightable works and also
@@ -1393,7 +1391,7 @@ The operator of an MMC Site may republish an MMC contained in the site
 under CC-BY-SA on the same site at any time before August 1, 2009,
 provided the MMC is eligible for relicensing.
 
-@strong{ADDENDUM: How to use this License for your documents}
+`ADDENDUM: How to use this License for your documents'
 
 To use this License in a document you have written, include a copy of
 the License in the document and put the following copyright and