pragma Precondition ( [Check =>] Boolean_Expression [,[Message =>] String_Expression]);
Precondition pragma is similar to
except that the corresponding checks take place immediately upon
entry to the subprogram, and if a precondition fails, the exception
is raised in the context of the caller, and the attribute 'Result
cannot be used within the precondition expression.
Otherwise, the placement and visibility rules are identical to those described for postconditions. The following is an example of use within a package spec:
package Math_Functions is ... function Sqrt (Arg : Float) return Float; pragma Precondition (Arg >= 0.0) ... end Math_Functions;
Precondition pragmas may appear either immediately 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.