diff options
Diffstat (limited to 'gcc/ada/gnat_rm.texi')
| -rw-r--r-- | gcc/ada/gnat_rm.texi | 167 |
1 files changed, 91 insertions, 76 deletions
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 29ba674..ce5a35d 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -1229,47 +1229,69 @@ addition. @node Pragma Assertion_Policy @unnumberedsec Pragma Assertion_Policy -@findex Debug_Policy +@findex Assertion_Policy @noindent Syntax: - @smallexample @c ada pragma Assertion_Policy (CHECK | DISABLE | IGNORE); + +Pragma Assertion_Policy ( + ASSERTION_KIND => POLICY_IDENTIFIER + @{, ASSERTION_KIND => POLICY_IDENTIFIER@}); + +ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND + +RM_ASSERTION_KIND ::= Assert | + Static_Predicate | + Dynamic_Predicate | + Pre | + Pre'Class | + Post | + Post'Class | + Type_Invariant | + Type_Invariant'Class + +ID_ASSERTION_KIND ::= Assert_And_Cut | + Assume | + Contract_Cases | + Debug | + Invariant | + Invariant'Class | + Loop_Invariant | + Loop_Variant | + Postcondition | + Precondition | + Predicate + +POLICY_IDENTIFIER ::= Check | Disable | Ignore @end smallexample @noindent -This is a standard Ada 2005 pragma that is available as an +This is a standard Ada 2012 pragma that is available as an implementation-defined pragma in earlier versions of Ada. - -If the argument is @code{CHECK}, then assertions are enabled. -If the argument is @code{IGNORE}, then assertions are ignored. +The assertion kinds @code{RM_ASSERTION_KIND} are those defined in +the Ada standard. The assertion kinds @code{ID_ASSERTION_KIND} +are implementation defined additions recognized by the GNAT compiler. + +The pragma applies in both cases to pragmas and aspects with matching +names, e.g. @code{Pre} applies to the Pre aspect, and @code{Precondition} +applies to both the @code{Precondition} pragma +and the aspect @code{Precondition}. + +If the policy is @code{CHECK}, then assertions are enabled, i.e. +the corresponding pragma or aspect is activated. +If the policy is @code{IGNORE}, then assertions are ignored, i.e. +the corresponding pragma or aspect is deactivated. This pragma overrides the effect of the @option{-gnata} switch on the command line. -Assertions are of three kinds: - -@itemize @bullet -@item -Pragma @code{Assert}. -@item -In Ada 2012, all assertions defined in the RM as aspects: preconditions, -postconditions, type invariants and (sub)type predicates. -@item -Corresponding pragmas for type invariants and (sub)type predicates. -@end itemize - The implementation defined policy @code{DISABLE} is like @code{IGNORE} except that it completely disables semantic -checking of the argument to @code{pragma Assert}. This may -be useful when the pragma argument references subprograms +checking of the corresponding pragma or aspect. This is +useful when the pragma or aspect argument references subprograms in a with'ed package which is replaced by a dummy package for the final build. -Note: this is a standard language-defined pragma in versions -of Ada from 2005 on. In GNAT, it is implemented in all versions -of Ada, and the DISABLE policy is an implementation-defined -addition. - @node Pragma Assume_No_Invalid_Values @unnumberedsec Pragma Assume_No_Invalid_Values @findex Assume_No_Invalid_Values @@ -1416,9 +1438,12 @@ passing mechanisms on a parameter by parameter basis. Syntax: @smallexample @c ada pragma Check ( - [Name =>] Identifier, + [Name =>] CHECK_KIND, [Check =>] Boolean_EXPRESSION [, [Message =>] string_EXPRESSION] ); + +CHECK_KIND ::= IDENTIFIER | + Pre'Class | Post'Class | Type_Invariant'Class @end smallexample @noindent @@ -1426,10 +1451,7 @@ This pragma is similar to the predefined pragma @code{Assert} except that an extra identifier argument is present. In conjunction with pragma @code{Check_Policy}, this can be used to define groups of assertions that can be independently controlled. The identifier @code{Assertion} is special, it -refers to the normal set of pragma @code{Assert} statements. The identifiers -@code{Precondition} and @code{Postcondition} correspond to the pragmas of these -names, so these three names would normally not be used directly in a pragma -@code{Check}. +refers to the normal set of pragma @code{Assert} statements. Checks introduced by this pragma are normally deactivated by default. They can be activated either by the command line option @option{-gnata}, which turns on @@ -1532,22 +1554,40 @@ switches (in particular -gnatp) in the usual manner. Syntax: @smallexample @c ada pragma Check_Policy - ([Name =>] Identifier, + ([Name =>] CHECK_KIND, [Policy =>] POLICY_IDENTIFIER); +CHECK_KIND ::= IDENTIFIER | + Pre'Class | Post'Class | Type_Invariant'Class + POLICY_IDENTIFIER ::= ON | OFF | CHECK | DISABLE | IGNORE @end smallexample @noindent -This pragma is similar to the predefined pragma @code{Assertion_Policy}, -except that it controls sets of named assertions introduced using the -@code{Check} pragmas. It can be used as a configuration pragma or (unlike -@code{Assertion_Policy}) can be used within a declarative part, in which case -it controls the status to the end of the corresponding construct (in a manner -identical to pragma @code{Suppress)}. +This pragma is used to set the checking policy for assertions (specified +by aspects of pragmas), the @code{Debug} pragma, or additional checks +to be checked using the @code{Check} pragma. It may appear either as +a configuration pragma, or within a declarative part of package. In the +latter case, it applies from the point where it appears to the end of +the declarative region (like pragma @code{Suppress}). -The identifier given as the first argument corresponds to a name used in -associated @code{Check} pragmas. For example, if the pragma: +The @code{Check_Policy} pragma is similar to the +predefined @code{Assertion_Policy} pragma, +and if the first argument corresponds to one of the assertion kinds that +are allowed by @code{Assertion_Policy}, then the effect is identical. +The identifiers @code{Precondition} and @code{Postcondition} are allowed +synonyms for @code{Pre} and @code{Post}. + +If the first argument is Debug, then the policy applies to Debug pragmas, +disabling their effect if the policy is @code{Off}, @code{Disable}, or +@code{Ignore}, and allowing them to execute with normal semantics if +the policy is @code{On} or @code{Check}. In addition if the policy is +@code{Disable}, then the procedure call in @code{Debug} pragmas will +be totally ignored and not analyzed semanticslly. + +Finally the first argument may be some other identifier than the above +posibilities, in which case it controls a set of named assertions +that can be checked using pragma @code{Check}. For example, if the pragma: @smallexample @c ada pragma Check_Policy (Critical_Error, OFF); @@ -1555,37 +1595,19 @@ pragma Check_Policy (Critical_Error, OFF); @noindent is given, then subsequent @code{Check} pragmas whose first argument is also -@code{Critical_Error} will be disabled. The special identifier @code{Assertion} -controls the behavior of normal assertions (thus a pragma -@code{Check_Policy} with this identifier is similar to the normal -@code{Assertion_Policy} pragma except that it can appear within a -declarative part). - -The special identifiers @code{Precondition} and @code{Postcondition} control -the status of preconditions and postconditions given as pragmas. -If a @code{Precondition} pragma -is encountered, it is ignored if turned off by a @code{Check_Policy} specifying -that @code{Precondition} checks are @code{Off} or @code{Ignored}. Similarly use -of the name @code{Postcondition} controls whether @code{Postcondition} pragmas -are recognized. Note that preconditions and postconditions given as aspects -are controlled differently, either by the @code{Assertion_Policy} pragma or -by the @code{Check_Policy} pragma with identifier @code{Assertion}. +@code{Critical_Error} will be disabled. The check policy is @code{OFF} to turn off corresponding checks, and @code{ON} to turn on corresponding checks. The default for a set of checks for which no @code{Check_Policy} is given is @code{OFF} unless the compiler switch @option{-gnata} is given, which turns on all checks by default. -The check policy settings @code{CHECK} and @code{IGNORE} are also recognized +The check policy settings @code{CHECK} and @code{IGNORE} are recognized as synonyms for @code{ON} and @code{OFF}. These synonyms are provided for -compatibility with the standard @code{Assertion_Policy} pragma. - -The implementation defined policy @code{DISABLE} is like -@code{OFF} except that it completely disables semantic -checking of the argument to the corresponding class of -pragmas. This may be useful when the pragma arguments reference -subprograms in a with'ed package which is replaced by a dummy package -for the final build. +compatibility with the standard @code{Assertion_Policy} pragma. The check +policy setting @code{DISABLE} is also synonymous with @code{OFF} in this +context, but does not have any other significance for check +names other than assertion kinds. @node Pragma Comment @unnumberedsec Pragma Comment @@ -2113,7 +2135,8 @@ corresponding to the argument with a terminating semicolon. Pragmas are permitted in sequences of declarations, so you can use pragma @code{Debug} to intersperse calls to debug procedures in the middle of declarations. Debug pragmas can be enabled either by use of the command line switch @option{-gnata} -or by use of the configuration pragma @code{Debug_Policy}. +or by use of the pragma @code{Check_Policy} with a first argument of +@code{Debug}. @node Pragma Debug_Policy @unnumberedsec Pragma Debug_Policy @@ -2122,21 +2145,13 @@ or by use of the configuration pragma @code{Debug_Policy}. Syntax: @smallexample @c ada -pragma Debug_Policy (CHECK | DISABLE | IGNORE); +pragma Debug_Policy (CHECK | DISABLE | IGNORE | ON | OFF); @end smallexample @noindent -If the argument is @code{CHECK}, then pragma @code{DEBUG} is enabled. -If the argument is @code{IGNORE}, then pragma @code{DEBUG} is ignored. -This pragma overrides the effect of the @option{-gnata} switch on the -command line. - -The implementation defined policy @code{DISABLE} is like -@code{IGNORE} except that it completely disables semantic -checking of the argument to @code{pragma Debug}. This may -be useful when the pragma argument references subprograms -in a with'ed package which is replaced by a dummy package -for the final build. +This pragma is equivalent to a corresponding @code{Check_Policy} pragma +with a first argument of @code{Debug}. It is retained for historical +compatibility reasons. @node Pragma Default_Storage_Pool @unnumberedsec Pragma Default_Storage_Pool |