9
GCC 14 release brings Ada/GNAT improvements
(gcc.gnu.org)
- New implementation-defined aspects and pragmas:
Local_Restrictions, 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.User_Aspect_DefinitionandUser_Aspect, which provide a mechanism for avoiding textual duplication if some set of aspect specifications is needed in multiple places.
- New implementation-defined aspects and pragmas for verification of the SPARK 2014 subset of Ada:
Always_Terminates, which provides a condition for a subprogram to necessarily complete (either return normally or raise an exception).Ghost_Predicate, which introduces a subtype predicate that can reference Ghost entities.Exceptional_Cases, 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.Side_Effects, which indicates that a function should be handled like a procedure with respect to parameter modes,Globalcontract, exceptional contract and termination: it may have output parameters, write global variables, raise exceptions and not terminate.
- 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.
- Support for the LoongArch architecture.
- Support for vxWorks 7 Cert RTP has been removed.
- Additional hardening improvements. For more information reltated to hardening options, refer to the GCC Instrumentation Options and the GNAT Reference Manual, Security and Hardening Features.
- Improve style checking for redundant parentheses with
-gnatyz - New switch
-gnateHto force reverse Bit_Order threshold to 64. - Experimental features:
- Storage Model: 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.
- String Interpolation: allows for easier string formatting. Further clean up and improvements to the GNAT code.