* [COMMITTED] gcc-14: Add Ada changes
@ 2024-04-26 8:55 Marc Poulhiès
2024-04-26 13:17 ` Marek Polacek
0 siblings, 1 reply; 3+ messages in thread
From: Marc Poulhiès @ 2024-04-26 8:55 UTC (permalink / raw)
To: gcc-patches; +Cc: Marc Poulhiès, Fernando Oleo Blanco, Piotr Trojanek
Co-authored-by: Fernando Oleo Blanco <irvise_ml@irvise.xyz>
Co-authored-by: Piotr Trojanek <trojanek@adacore.com>
Signed-off-by: Marc Poulhiès <poulhies@adacore.com>
---
htdocs/gcc-14/changes.html | 67 +++++++++++++++++++++++++++++++++++++-
1 file changed, 66 insertions(+), 1 deletion(-)
diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html
index 83b1016c..87e04cb8 100644
--- a/htdocs/gcc-14/changes.html
+++ b/htdocs/gcc-14/changes.html
@@ -239,7 +239,72 @@ a work-in-progress.</p>
</li>
</ul>
-<!-- <h3 id="ada">Ada</h3> -->
+<h3 id="ada">Ada</h3>
+
+<ul>
+ <li>New implementation-defined aspects and pragmas:
+ <ul>
+ <li><a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Aspect-Local_005fRestrictions.html"><code>Local_Restrictions</code></a>,
+ which 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/gnat_rm/Pragma-User_005fAspect_005fDefinition.html"><code>User_Aspect_Definition</code></a>
+ and <a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Aspect-User_005fAspect.html"><code>User_Aspect</code></a>,
+ which 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/gnat_rm/Aspect-Always_005fTerminates.html"><code>Always_Terminates</code></a>,
+ which 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/gnat_rm/Aspect-Ghost_005fPredicate.html"><code>Ghost_Predicate</code></a>,
+ which introduces a subtype predicate that can reference Ghost entities.
+ </li>
+ <li><a href="https://gcc.gnu.org/onlinedocs/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>
+ <li><a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Aspect-Side_005fEffects.html"><code>Side_Effects</code></a>,
+ which 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>
+ </ul>
+ </li>
+ <li>The new attributes and contracts have been applied to the relevant parts
+ of the Ada runtime library, which has been subsequently proven to be correct
+ with SPARK 2014.</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>Support for vxWorks 7 Cert RTP has been removed.</li>
+ <li>Additional hardening improvements. For more information reltated to
+ hardening options, refer to
+ the <a href="https://gcc.gnu.org/onlinedocs/gcc/Instrumentation-Options.html#index-fharden-compares">GCC
+ Instrumentation Options</a> and
+ the <a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Security-Hardening-Features.html">GNAT
+ Reference Manual, Security and Hardening Features</a>.
+ </li>
+ <li>Improve style checking for redundant parentheses
+ with <a href="https://gcc.gnu.org/onlinedocs/gnat_ugn/Style-Checking.html#index--gnatyz-_0028gcc_0029"><code>-gnatyz</code></a></li>
+ <li>New
+ switch <a href="https://gcc.gnu.org/onlinedocs/gnat_ugn/Alphabetical-List-of-All-Switches.html#index--gnateH-_0028gcc_0029"><code>-gnateH</code></a>
+ to force reverse Bit_Order threshold to 64.</li>
+ <li>Experimental features:
+ <ul><a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Pragma-Storage_005fModel.html">Storage
+ Model</a>: this feature proposes to redesign the concepts of Storage Pools
+ into a more efficient model allowing higher performances and easier
+ integration with low footprint embedded run-times.</ul>
+ <ul><a href="https://gcc.gnu.org/onlinedocs/gnat_rm/String-interpolation.html">String
+ Interpolation</a>: allows for easier string formatting.</ul>
+ </li>
+ <li>Further clean up and improvements to the GNAT code.</li>
+</ul>
<!-- <h3 id="c-family">C family</h3> -->
--
2.43.2
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: [COMMITTED] gcc-14: Add Ada changes
2024-04-26 8:55 [COMMITTED] gcc-14: Add Ada changes Marc Poulhiès
@ 2024-04-26 13:17 ` Marek Polacek
2024-04-26 13:25 ` Marc Poulhiès
0 siblings, 1 reply; 3+ messages in thread
From: Marek Polacek @ 2024-04-26 13:17 UTC (permalink / raw)
To: Marc Poulhiès; +Cc: gcc-patches, Fernando Oleo Blanco, Piotr Trojanek
On Fri, Apr 26, 2024 at 10:55:35AM +0200, Marc Poulhiès wrote:
> Co-authored-by: Fernando Oleo Blanco <irvise_ml@irvise.xyz>
> Co-authored-by: Piotr Trojanek <trojanek@adacore.com>
> Signed-off-by: Marc Poulhiès <poulhies@adacore.com>
> ---
> htdocs/gcc-14/changes.html | 67 +++++++++++++++++++++++++++++++++++++-
> 1 file changed, 66 insertions(+), 1 deletion(-)
>
> diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html
> index 83b1016c..87e04cb8 100644
> --- a/htdocs/gcc-14/changes.html
> +++ b/htdocs/gcc-14/changes.html
> @@ -239,7 +239,72 @@ a work-in-progress.</p>
> </li>
> </ul>
>
> -<!-- <h3 id="ada">Ada</h3> -->
> +<h3 id="ada">Ada</h3>
> +
> +<ul>
> + <li>New implementation-defined aspects and pragmas:
> + <ul>
> + <li><a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Aspect-Local_005fRestrictions.html"><code>Local_Restrictions</code></a>,
> + which 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/gnat_rm/Pragma-User_005fAspect_005fDefinition.html"><code>User_Aspect_Definition</code></a>
> + and <a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Aspect-User_005fAspect.html"><code>User_Aspect</code></a>,
> + which 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/gnat_rm/Aspect-Always_005fTerminates.html"><code>Always_Terminates</code></a>,
> + which 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/gnat_rm/Aspect-Ghost_005fPredicate.html"><code>Ghost_Predicate</code></a>,
> + which introduces a subtype predicate that can reference Ghost entities.
> + </li>
> + <li><a href="https://gcc.gnu.org/onlinedocs/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>
> + <li><a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Aspect-Side_005fEffects.html"><code>Side_Effects</code></a>,
> + which 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>
> + </ul>
> + </li>
> + <li>The new attributes and contracts have been applied to the relevant parts
> + of the Ada runtime library, which has been subsequently proven to be correct
> + with SPARK 2014.</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>Support for vxWorks 7 Cert RTP has been removed.</li>
> + <li>Additional hardening improvements. For more information reltated to
> + hardening options, refer to
> + the <a href="https://gcc.gnu.org/onlinedocs/gcc/Instrumentation-Options.html#index-fharden-compares">GCC
> + Instrumentation Options</a> and
> + the <a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Security-Hardening-Features.html">GNAT
> + Reference Manual, Security and Hardening Features</a>.
> + </li>
> + <li>Improve style checking for redundant parentheses
> + with <a href="https://gcc.gnu.org/onlinedocs/gnat_ugn/Style-Checking.html#index--gnatyz-_0028gcc_0029"><code>-gnatyz</code></a></li>
> + <li>New
> + switch <a href="https://gcc.gnu.org/onlinedocs/gnat_ugn/Alphabetical-List-of-All-Switches.html#index--gnateH-_0028gcc_0029"><code>-gnateH</code></a>
> + to force reverse Bit_Order threshold to 64.</li>
> + <li>Experimental features:
> + <ul><a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Pragma-Storage_005fModel.html">Storage
> + Model</a>: this feature proposes to redesign the concepts of Storage Pools
> + into a more efficient model allowing higher performances and easier
> + integration with low footprint embedded run-times.</ul>
> + <ul><a href="https://gcc.gnu.org/onlinedocs/gnat_rm/String-interpolation.html">String
> + Interpolation</a>: allows for easier string formatting.</ul>
> + </li>
> + <li>Further clean up and improvements to the GNAT code.</li>
> +</ul>
Some of this doesn't pass https://validator.w3.org/. Please take a look
when you get a chance. Thanks,
Marek
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: [COMMITTED] gcc-14: Add Ada changes
2024-04-26 13:17 ` Marek Polacek
@ 2024-04-26 13:25 ` Marc Poulhiès
0 siblings, 0 replies; 3+ messages in thread
From: Marc Poulhiès @ 2024-04-26 13:25 UTC (permalink / raw)
To: Marek Polacek; +Cc: gcc-patches, Fernando Oleo Blanco, Piotr Trojanek
Marek Polacek <polacek@redhat.com> writes:
Hello,
>> + <li>Experimental features:
>> + <ul><a href="https://gcc.gnu.org/onlinedocs/gnat_rm/Pragma-Storage_005fModel.html">Storage
>> + Model</a>: this feature proposes to redesign the concepts of Storage Pools
>> + into a more efficient model allowing higher performances and easier
>> + integration with low footprint embedded run-times.</ul>
>> + <ul><a href="https://gcc.gnu.org/onlinedocs/gnat_rm/String-interpolation.html">String
>> + Interpolation</a>: allows for easier string formatting.</ul>
>> + </li>
>> + <li>Further clean up and improvements to the GNAT code.</li>
>> +</ul>
>
> Some of this doesn't pass https://validator.w3.org/. Please take a look
> when you get a chance. Thanks,
Sorry about that. I've pushed the simple fix and checked the validator
is happy again. Thanks for the notice.
Marc
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2024-04-26 13:25 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2024-04-26 8:55 [COMMITTED] gcc-14: Add Ada changes Marc Poulhiès
2024-04-26 13:17 ` Marek Polacek
2024-04-26 13:25 ` Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).