@@ -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