Fernando Oleo Blanco <irvise...@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> -->
