On Fri, 26 Apr 2024, Marc Poulhiès wrote:
> Co-authored-by: Fernando Oleo Blanco <irvise...@irvise.xyz>
> Co-authored-by: Piotr Trojanek <troja...@adacore.com>
> Signed-off-by: Marc Poulhiès <poulh...@adacore.com>
> ---
> htdocs/gcc-14/changes.html | 67 +++++++++++++++++++++++++++++++++++++-
This is really great how thoroughly you documented all these changes -
thanks to the three of you!
Below is a little follow-up I'd like to propose: It mostly simplifies
the structure of bullet items a bit and changes "it may have output
parameters ... and not terminate" to "it may have output parameters ...
and fail to terminate", the former somehow feeling odd for me to read.
What do you think?
Gerald
diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html
index aa1d97a8..03c4bd18 100644
--- a/htdocs/gcc-14/changes.html
+++ b/htdocs/gcc-14/changes.html
@@ -246,35 +246,35 @@ You may also want to check out our
<ul>
<li>New implementation-defined aspects and pragmas:
<ul>
- <li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-Local_005fRestrictions.html";><code>Local_Restrictions</code></a>,
- which specifies that a particular subprogram does not violate one or more
+ <li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-Local_005fRestrictions.html";><code>Local_Restrictions</code></a>
+ specifies that a particular subprogram does not violate one or more
local restrictions, nor can it call a subprogram that is not subject to
the same requirements.</li>
<li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Pragma-User_005fAspect_005fDefinition.html";><code>User_Aspect_Definition</code></a>
- and <a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-User_005fAspect.html";><code>User_Aspect</code></a>,
- which provide a mechanism for avoiding textual duplication if some set of
+ and <a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-User_005fAspect.html";><code>User_Aspect</code></a>
+ provide a mechanism for avoiding textual duplication if some set of
aspect specifications is needed in multiple places.</li>
</ul>
</li>
<li>New implementation-defined aspects and pragmas for verification of the
SPARK 2014 subset of Ada:
<ul>
- <li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-Always_005fTerminates.html";><code>Always_Terminates</code></a>,
- which provides a condition for a subprogram to necessarily complete
+ <li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-Always_005fTerminates.html";><code>Always_Terminates</code></a>
+ provides a condition for a subprogram to necessarily complete
(either return normally or raise an exception).</li>
- <li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-Ghost_005fPredicate.html";><code>Ghost_Predicate</code></a>,
- which introduces a subtype predicate that can reference Ghost entities.
+ <li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-Ghost_005fPredicate.html";><code>Ghost_Predicate</code></a>
+ introduces a subtype predicate that can reference Ghost entities.
</li>
- <li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-Exceptional_005fCases.html";><code>Exceptional_Cases</code></a>,
- which lists exceptions that might be propagated by the subprogram with
- side effects in the context of its precondition and associates them with
a
- specific postcondition.
+ <li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-Exceptional_005fCases.html";><code>Exceptional_Cases</code></a>
+ lists exceptions that might be propagated by the subprogram with
+ side effects in the context of its precondition and associates them
+ with a specific postcondition.
</li>
- <li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-Side_005fEffects.html";><code>Side_Effects</code></a>,
- which indicates that a function should be handled like a procedure with
+ <li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Aspect-Side_005fEffects.html";><code>Side_Effects</code></a>
+ indicates that a function should be handled like a procedure with
respect to parameter modes, Global contract, exceptional contract and
termination: it may have output parameters, write global variables, raise
- exceptions and not terminate.</li>
+ exceptions and fail to terminate.</li>
</ul>
</li>
<li>The new attributes and contracts have been applied to the relevant parts
@@ -297,7 +297,7 @@ You may also want to check out our
<li>Experimental features:
<ul>
<li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/Pragma-Storage_005fModel.html";>Storage
- Model</a>: this feature proposes to redesign the concepts of Storage
Pools
+ Model</a>: proposes to redesign the concepts of Storage Pools
into a more efficient model allowing higher performance and easier
integration with low footprint embedded runtimes.</li>
<li><a
href="https://gcc.gnu.org/onlinedocs/gcc-14.1.0/gnat_rm/String-interpolation.html";>String
