[wwwdocs] Add Ada's GCC 14 changelog entry
Checks
Commit Message
Dear all,
just like last year, I would like to commit the changes that took place
over at GNAT for GCC v14. The patch is attached to the email. Hopefully
it is good enough to just be added to master. If you see something wrong
or if you would like to add anything to it, feel free :) Feedback is
always welcomed.
Best regards,
Fer
Comments
Fernando Oleo Blanco <irvise_ml@irvise.xyz> writes:
> Dear all,
>
> just like last year, I would like to commit the changes that took place
> over at GNAT for GCC v14. The patch is attached to the email. Hopefully
> it is good enough to just be added to master. If you see something wrong
> or if you would like to add anything to it, feel free :) Feedback is
> always welcomed.
Fernando,
Thank you for this work! I have a few comments, see below.
diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html
index 85ccc54d..e6c96c9f 100644
--- a/htdocs/gcc-14/changes.html
+++ b/htdocs/gcc-14/changes.html
@@ -171,7 +171,49 @@ a work-in-progress.</p>
<!-- .................................................................. -->
<h2 id="languages">New Languages and Language specific improvements</h2>
-<!-- <h3 id="ada">Ada</h3> -->
+<h3 id="ada">Ada</h3>
+
+<ul>
+ <li>Several new aspects and contracts have been implemented:
Maybe worth noting that these are implementation defined aspects.
+ <ul>
+ <li><code>Exceptional_Cases</code> may be specified for procedures and
+ functions with side effects; it can be used to list exceptions that might
+ be propagated by the subprogram with side effects in the context of its
+ precondition, and associate them with a specific postcondition. For more
+ information, refer to SPARK 2014 Reference Manual, section 6.1.9.</li>
+ <li><code>User_Aspect</code> takes an argument that is the name of an
+ aspect defined by a User_Aspect_Definition configuration pragma.</li>
+ <li><code>Local_Restrictions</code> is used to specify 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><code>Side_Effects</code> is equivalent to <code>pragma
+ Side_Effecs</code>.</li>
+ <li><code>Always_Terminates</code> is a boolean equivalent to <code>pragma
+ Always_Terminates</code></li>
+ <li><code>Ghost_Predicate</code></li>
It looks like Ghost_Predicate is missing some text here.
It may be a good thing to link to the actual documentation for these
options. Thanks to some documention changes, we can now link to
an option directly. For example:
https://gcc.gnu.org/onlinedocs/gnat_rm/Implementation-Defined-Pragmas.html
You would need to point to the correct version (this one points to
current devel version).
+ </ul>
+ </li>
+ <li>The new attributes and contracts have been applied to the relevant parts
+ of the Ada library and more code has been proven to be correct.</li>
+ <li>Initial support for the
+ <a href="https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/"><code>CHERI</code></a>
+ architecture.</li>
+ <li>Support for the <code>LoongArch</code> architecture.</li>
+ <li>Hardening improvements:
+ <ul>
+ <li>Use of the new <code>-fharden*</code> options. Most
+ notably <code>-fharden-compares</code>,
+ <code>-fharden-conditional-branches</code> and
+ <code>-fharden-control-flow-redundancy</code>.</li>
+ <li>Custom bools with higher Hamming distance.</li>
+ <li>The <code>strub</code> attribute has been added for functions and
Same as above for doc links:
https://gcc.gnu.org/onlinedocs/gcc/Instrumentation-Options.html#index-fharden-compares
+ variables in order to automatically zero-out their stack upon use or
+ return.</li>
+ </ul>
+ </li>
+ <li>Further clean up and improvements to the GNAT code.</li>
+ <li>Support for vxWorks 7 Cert RTP has been removed.</li>
+</ul>
<!-- <h3 id="c-family">C family</h3> -->
Hi Mark,
On 2/26/24 10:17, Marc Poulhiès wrote:
>
> Fernando,
>
> Thank you for this work! I have a few comments, see below.
>
> diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html
> index 85ccc54d..e6c96c9f 100644
> --- a/htdocs/gcc-14/changes.html
> +++ b/htdocs/gcc-14/changes.html
> @@ -171,7 +171,49 @@ a work-in-progress.</p>
> <!-- .................................................................. -->
> <h2 id="languages">New Languages and Language specific improvements</h2>
>
> -<!-- <h3 id="ada">Ada</h3> -->
> +<h3 id="ada">Ada</h3>
> +
> +<ul>
> + <li>Several new aspects and contracts have been implemented:
>
> Maybe worth noting that these are implementation defined aspects.
Noted
>
> + <ul>
> + <li><code>Exceptional_Cases</code> may be specified for procedures and
[...]
> + Side_Effecs</code>.</li>
> + <li><code>Always_Terminates</code> is a boolean equivalent to <code>pragma
> + Always_Terminates</code></li>
> + <li><code>Ghost_Predicate</code></li>
>
> It looks like Ghost_Predicate is missing some text here.
>
> It may be a good thing to link to the actual documentation for these
> options. Thanks to some documention changes, we can now link to
> an option directly. For example:
>
> https://gcc.gnu.org/onlinedocs/gnat_rm/Implementation-Defined-Pragmas.html
Added
>
> You would need to point to the correct version (this one points to
> current devel version).
>
Done
> + </ul>
> + </li>
> + <li>The new attributes and contracts have been applied to the relevant parts
[...]
> + <code>-fharden-control-flow-redundancy</code>.</li>
> + <li>Custom bools with higher Hamming distance.</li>
> + <li>The <code>strub</code> attribute has been added for functions and
>
> Same as above for doc links:
>
> https://gcc.gnu.org/onlinedocs/gcc/Instrumentation-Options.html#index-fharden-compares
Done
>
> + variables in order to automatically zero-out their stack upon use or
> + return.</li>
> + </ul>
> + </li>
> + <li>Further clean up and improvements to the GNAT code.</li>
> + <li>Support for vxWorks 7 Cert RTP has been removed.</li>
> +</ul>
>
> <!-- <h3 id="c-family">C family</h3> -->
I have applied your recommendations. The documentation links are still
not up... Nonetheless, I created the URL in such a way that they should
work once the final documentation is given a release number (which I
guessed to be 14.1.0). If you think this can be improved just say so.
Nonetheless, feel free to modify my patch if you see it fit.
Best regards,
Fer
From 0ae94649be7f638bb4f98ba3e2ba2e1bf9770c09 Mon Sep 17 00:00:00 2001
From: Fernando Oleo Blanco <irvise@irvise.xyz>
Date: Sun, 25 Feb 2024 21:43:43 +0100
Subject: [PATCH 1/1] Add Ada changes for v14
---
htdocs/gcc-14/changes.html | 44 +++++++++++++++++++++++++++++++++++++-
1 file changed, 43 insertions(+), 1 deletion(-)
@@ -171,7 +171,49 @@ a work-in-progress.</p>
<!-- .................................................................. -->
<h2 id="languages">New Languages and Language specific improvements</h2>
-<!-- <h3 id="ada">Ada</h3> -->
+<h3 id="ada">Ada</h3>
+
+<ul>
+ <li>Several new aspects and contracts have been implemented:
+ <ul>
+ <li><code>Exceptional_Cases</code> may be specified for procedures and
+ functions with side effects; it can be used to list exceptions that might
+ be propagated by the subprogram with side effects in the context of its
+ precondition, and associate them with a specific postcondition. For more
+ information, refer to SPARK 2014 Reference Manual, section 6.1.9.</li>
+ <li><code>User_Aspect</code> takes an argument that is the name of an
+ aspect defined by a User_Aspect_Definition configuration pragma.</li>
+ <li><code>Local_Restrictions</code> is used to specify 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><code>Side_Effects</code> is equivalent to <code>pragma
+ Side_Effecs</code>.</li>
+ <li><code>Always_Terminates</code> is a boolean equivalent to <code>pragma
+ Always_Terminates</code></li>
+ <li><code>Ghost_Predicate</code></li>
+ </ul>
+ </li>
+ <li>The new attributes and contracts have been applied to the relevant parts
+ of the Ada library and more code has been proven to be correct.</li>
+ <li>Initial support for the
+ <a href="https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/"><code>CHERI</code></a>
+ architecture.</li>
+ <li>Support for the <code>LoongArch</code> architecture.</li>
+ <li>Hardening improvements:
+ <ul>
+ <li>Use of the new <code>-fharden*</code> options. Most
+ notably <code>-fharden-compares</code>,
+ <code>-fharden-conditional-branches</code> and
+ <code>-fharden-control-flow-redundancy</code>.</li>
+ <li>Custom bools with higher Hamming distance.</li>
+ <li>The <code>strub</code> attribute has been added for functions and
+ variables in order to automatically zero-out their stack upon use or
+ return.</li>
+ </ul>
+ </li>
+ <li>Further clean up and improvements to the GNAT code.</li>
+ <li>Support for vxWorks 7 Cert RTP has been removed.</li>
+</ul>
<!-- <h3 id="c-family">C family</h3> -->
--
2.43.2