end Sort;
@end smallexample
+@noindent
+Note: postcondition pragmas associated with subprograms that are
+marked as Inline_Always, or those marked as Inline with front-end
+inlining (-gnatN option set) are accepted and legality-checked
+by the compiler, but are ignored at run-time even if postcondition
+checking is enabled.
+
@node Pragma Precondition
@unnumberedsec Pragma Precondition
@cindex Preconditions
end Math_Functions;
@end smallexample
-@code{Postcondition} pragmas may appear either immediate following the
+@noindent
+@code{Precondition} pragmas may appear either immediate following the
(separate) declaration of a subprogram, or at the start of the
declarations of a subprogram body. Only other pragmas may intervene
(that is appear between the subprogram declaration and its
postconditions, or appear before the postcondition in the
declaration sequence in a subprogram body).
+Note: postcondition pragmas associated with subprograms that are
+marked as Inline_Always, or those marked as Inline with front-end
+inlining (-gnatN option set) are accepted and legality-checked
+by the compiler, but are ignored at run-time even if postcondition
+checking is enabled.
+
+
+
@node Pragma Profile (Ravenscar)
@unnumberedsec Pragma Profile (Ravenscar)
@findex Ravenscar
it is necessary to compile in optimizing mode.
@cindex @option{-gnatN} switch
-The use of @option{-gnatN} activates a more extensive inlining optimization
+The use of @option{-gnatN} activates inlining optimization
that is performed by the front end of the compiler. This inlining does
not require that the code generation be optimized. Like @option{-gnatn},
the use of this switch generates additional dependencies.
@option{-gnatN} automatically implies @option{-gnatn} so it is not necessary
to specify both options.
+When using a gcc-based back end (in practice this means using any version
+of GNAT other than the JGNAT, .NET or GNAAMP versions), then the use of
+@option{-gnatN} is deprecated, and the use of @option{-gnatn} is preferred.
+Historically front end inlining was more extensive than the gcc back end
+inlining, but that is no longer the case.
+
@item
If an object file @file{O} depends on the proper body of a subunit through
inlining or instantiation, it depends on the parent unit of the subunit.