23.6.1 Using pragma Annotate to Control Rule Exemption

Rule exemption is controlled by pragma Annotate when its first argument is “gnatcheck”. The syntax of gnatcheck's exemption control annotations is as follows:

     pragma Annotate (gnatcheck, exemption_control, Rule_Name, [justification]);
     
     exemption_control ::= Exempt_On | Exempt_Off
     
     Rule_Name         ::= string_literal
     
     justification     ::= string_literal

When a gnatcheck annotation has more then four arguments, gnatcheck issues a warning and ignores the additional arguments. If the additional arguments do not follow the syntax above, gnatcheck emits a warning and ignores the annotation.

The Rule_Name argument should be the name of some existing gnatcheck rule. Otherwise a warning message is generated and the pragma is ignored. If Rule_Name denotes a rule that is not activated by the given gnatcheck call, the pragma is ignored and no warning is issued.

A source code section where an exemption is active for a given rule is delimited by an exempt_on and exempt_off annotation pair:

     pragma Annotate (gnatcheck, Exempt_On, Rule_Name, "justification");
     -- source code section
     pragma Annotate (gnatcheck, Exempt_Off, Rule_Name);