Next: , Previous:   [Contents][Index]

7 Rule exemption

One of the most useful applications of gnatcheck is to automate the enforcement of project-specific coding standards, for example in safety-critical systems where particular features must be restricted in order to simplify the certification effort. However, it may sometimes be appropriate to violate a coding standard rule, and in such cases the rationale for the violation should be provided in the source program itself so that the individuals reviewing or maintaining the program can immediately understand the intent.

The gnatcheck tool supports this practice with the notion of a “rule exemption” covering a specific source code section. Normally rule violation messages are issued both on stderr and in a report file. In contrast, exempted violations are not listed on stderr; thus users invoking gnatcheck interactively (e.g. in its GPS interface) do not need to pay attention to known and justified violations. However, exempted violations along with their justification are documented in a special section of the report file that gnatcheck generates.


Next: , Up: Rule exemption   [Contents][Index]

7.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 than 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. The exception from this rule is that exemption sections for Warnings rule are fully processed when Restrictions rule is activated.

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);

Previous: , Up: Rule exemption   [Contents][Index]

7.2 gnatcheck Annotations Rules


Previous: , Up: Rule exemption   [Contents][Index]