GNATcheck Reference Manual
**************************

GNATcheck Reference Manual
Coding Standard Verifier

The GNAT Pro Ada Compiler
GNAT Pro Version 7.0.0w
Configuration level: 180752
Date: 2011/10/29

Copyright (C) 2009, AdaCore

Permission is granted to copy, distribute and/or modify this document
under the terms of the GNU Free Documentation License, Version 1.1 or
any later version published by the Free Software Foundation; with the
Invariant Sections being "GNU Free Documentation License", with the
Front-Cover Texts being "GNATcheck Reference Manual", and with no
Back-Cover Texts.  A copy of the license is included in the section
entitled "GNU Free Documentation License".

About This Manual
*****************

The `gnatcheck' tool in GNAT Pro can be used to enforce coding
conventions by analyzing Ada source programs with respect to a set of
rules supplied at tool invocation.  This manual describes the complete
set of predefined rules that `gnatcheck' can take as input.

What This Manual Contains
=========================

This manual contains a description of `gnatcheck', an ASIS-based
utility that checks properties of Ada source files according to a given
set of semantic rules

   *  *note Introduction::, gives the general overview of the
     `gnatcheck' tool

     *note Format of the Report File::, describes the structure of the
     report file generated by `gnatcheck'

     *note General gnatcheck Switches::, describes switches control the
     general `gnatcheck' behavior

     *note gnatcheck Rule Options::, describes options used to control
     a set of rules to be checked by `gnatcheck'

     *note Adding the Results of Compiler Checks to gnatcheck Output::,
     explains how the results of the check performed by the GNAT
     compiler can be added to the report generated by `gnatcheck'

     *note Project-Wide Checks::, explains how to apply `gnatcheck' to
     all the sources of your project

     *note Rule exemption::, explains how to turn off a rule check for
     a specified fragment of a source file

     *note Predefined Rules::, contains a description of each predefined
     `gnatcheck' rule, organized into categories.

     *note Example of gnatcheck Usage::, contains a full example of
     `gnatcheck' usage

     *note List of Rules::, gives an alphabetized list of all
     predefined rules, for ease of reference.

The name of each rule (the "rule identifier") denotes the condition
that is detected and flagged by `gnatcheck'.  The rule identifier is
used as a parameter of the `+R' or `-R' switch to `gnatcheck'.

What You Should Know Before Reading This Manual
===============================================

You should be familiar with the Ada language and with the usage of
GNAT Pro in general; please refer to the `GNAT Pro User's Guide'.

1 Introduction
**************

The `gnatcheck' tool is an ASIS-based utility that checks properties of
Ada source files according to a given set of semantic rules.  

   In order to check compliance with a given rule, `gnatcheck' has to
semantically analyze the Ada sources.  Therefore, checks can only be
performed on legal Ada units. Moreover, when a unit depends
semantically upon units located outside the current directory, the
source search path has to be provided when calling `gnatcheck', either
through a specified project file or through `gnatcheck' switches as
described below.

   A number of rules are predefined in `gnatcheck' and are described
later in this chapter.  You can also add new rules, by modifying the
`gnatcheck' code and rebuilding the tool. In order to add a simple rule
making some local checks, a small amount of straightforward ASIS-based
programming is usually needed.

   Project support for `gnatcheck' is provided by the GNAT driver (see
`The GNAT Driver and Project Files' section in `GNAT Pro User's Guide').

   Invoking `gnatcheck' on the command line has the form:

     $ gnatcheck [SWITCHES]  {FILENAME}
           [-files={ARG_LIST_FILENAME}]
           [-cargs GCC_SWITCHES] -rules RULE_OPTIONS

where
   * SWITCHES specify the general tool options

   * Each FILENAME is the name (including the extension) of a source
     file to process. "Wildcards" are allowed, and the file name may
     contain path information.

   * Each ARG_LIST_FILENAME is the name (including the extension) of a
     text file containing the names of the source files to process,
     separated by spaces or line breaks.

   * GCC_SWITCHES is a list of switches for `gcc'. They will be passed
     on to all compiler invocations made by `gnatcheck' to generate the
     ASIS trees. Here you can provide `-I' switches to form the source
     search path, and use the `-gnatec' switch to set the configuration
     file, use the `-gnat05' switch if sources should be compiled in
     Ada 2005 mode etc.

   * RULE_OPTIONS is a list of options for controlling a set of rules
     to be checked by `gnatcheck' (*note gnatcheck Rule Options::).

Either a `FILENAME' or an `ARG_LIST_FILENAME' must be supplied.

2 Format of the Report File
***************************

The `gnatcheck' tool outputs on `stderr' all messages concerning rule
violations except if running in quiet mode.  It also creates a text file
that contains the complete report of the last gnatcheck run. By default
this file is named `gnatcheck.out' and it is located in the current
directory; the `-o' option can be used to change the name and/or
location of the report file. This report contains:

   * general details of the `gnatcheck' run: date and time of the run,
     the version of the tool that has generated this report, full
     parameters of the  `gnatcheck' invocation, reference to the list
     of checked sources and applied rules (coding standard);

   * summary of the run (number of checked sources and detected
     violations);

   * list of exempted coding standard violations;

   * list of non-exempted coding standard violations;

   * list of problems in the definition of exemption sections;

   * list of language violations (compile-time errors) detected in
     processed sources;

3 General `gnatcheck' Switches
******************************

The following switches control the general `gnatcheck' behavior

`-a'
     Process all units including those with read-only ALI files such as
     those from the GNAT Run-Time library.

`-dX'
     Activate internal debugging switches. X is a letter or digit, or
     string of letters or digits, which specifies the type of debugging
     outputs desired. Normally these are used only for internal
     development or system debugging purposes. You can find full
     documentation for these switches in the body of the
     `ASIS_UL.Debug' unit in the ASIS Utility Library source file
     `asis_ul-debug.adb'.

`-h'
     List all the rules checked by the given `gnatcheck' version.

`-l'
     Use full source locations references in the report file. For a
     construct from a generic instantiation a full source location is a
     chain from the location of this construct in the generic unit to
     the place where this unit is instantiated.

`-log'
     Duplicate all the output sent to `stderr' into a log file. The log
     file is named `gnatcheck.log' and is located in the current
     directory.

`-mnnnn'
     Maximum number of diagnostics to be sent to `stdout', where nnnn
     is in the range 0...1000; the default value is 500. Zero means
     that there is no limitation on the number of diagnostic messages
     to be output.

`-q'
     Quiet mode. All the diagnostics about rule violations are placed
     in the `gnatcheck' report file only, without duplication on
     `stdout'.

`-s'
     Short format of the report file (no version information, no list
     of applied rules, no list of checked sources is included)

`--include-file=FILE'
     Append the content of the specified text file to the report file

`-t'
     Print out execution time.

`-v'
     Verbose mode; `gnatcheck' generates version information and then a
     trace of sources being processed.

`-o REPORT_FILE'
     Set name of report file file to REPORT_FILE .

`--write-rules=TEMPLATE_FILE'
     Write to TEMPLATE_FILE the template rule file that contains all
     the rules currently implemented in `gnatcheck' turned off. A user
     may edit this template file manually to get his own coding
     standard file.


4 `gnatcheck' Rule Options
**************************

The following options control the processing performed by `gnatcheck'.

`-ALL'
     Turn all the rule checks OFF.

`+RRULE_ID[:PARAM]'
     Turn on the check for a specified rule with the specified
     parameter, if any.  RULE_ID must be the identifier of one of the
     currently implemented rules (use `-h' for the list of implemented
     rules). Rule identifiers are not case-sensitive. The PARAM item
     must be a string representing a valid parameter(s) for the
     specified rule.  If it contains any space characters then this
     string must be enclosed in quotation marks.

`-RRULE_ID[:PARAM]'
     Turn off the check for a specified rule with the specified
     parameter, if any.

`-from=RULE_OPTION_FILENAME'
     Read the rule options from the text file RULE_OPTION_FILENAME,
     referred to as a "coding standard file" below.


The default behavior is that all the rule checks are disabled.

   If more then one rule option is specified for the same rule, these
options are summed together. If a new option contradicts the rule
settings specified by previous options for this rule, the new option
overrides the previous settings.

   A coding standard file is a text file that contains a set of rule
options described above.  The file may contain empty lines and
Ada-style comments (comment lines and end-of-line comments). There can
be several rule options on a single line (separated by a space).

   A coding standard file may reference other coding standard files by
including more `-from=RULE_OPTION_FILENAME' options, each such option
being replaced with the content of the corresponding coding standard
file during processing. In case a cycle is detected (that is,
`RULE_FILE_1' reads rule options from `RULE_FILE_2', and `RULE_FILE_2'
reads (directly or indirectly) rule options from `RULE_FILE_1'),
processing fails with an error message.

5 Adding the Results of Compiler Checks to `gnatcheck' Output
*************************************************************

The `gnatcheck' tool can include in the generated diagnostic messages
and in the report file the results of the checks performed by the
compiler. Though disabled by default, this effect may be obtained by
using `+R' with the following rule identifiers and parameters:

`Restrictions'
     To record restrictions violations (which are performed by the
     compiler if the pragma `Restrictions' or `Restriction_Warnings'
     are given), use the `Restrictions' rule with the same parameters
     as pragma `Restrictions' or `Restriction_Warnings'.

`Style_Checks'
     To record compiler style checks (see `Style Checking' section in
     `GNAT Pro User's Guide'), use the `Style_Checks' rule.  This rule
     takes a parameter in one of the following forms:
        * `All_Checks', which enables the standard style checks
          corresponding to the `-gnatyy' GNAT style check option, or

        * a string with the same structure and semantics as the
          `string_LITERAL' parameter of the GNAT pragma `Style_Checks'
          (for further information about this pragma, *note Pragma
          Style_Checks: (gnat_rm)Pragma Style_Checks.).

     For example, the `+RStyle_Checks:O' rule option activates the
     compiler style check that corresponds to `-gnatyO' style check
     option.

`Warnings'
     To record compiler warnings (see `Warning Message Control' section
     in `GNAT Pro User's Guide'), use the `Warnings' rule with a
     parameter that is a valid static_string_expression argument of the
     GNAT pragma `Warnings' (for further information about this pragma,
     *note Pragma Warnings: (gnat_rm)Pragma Warnings.).  Note that in
     case of gnatcheck 's' parameter, that corresponds to the GNAT
     `-gnatws' option, disables all the specific warnings, but not
     suppresses the warning mode, and 'e' parameter, corresponding to
     `-gnatwe' that means "treat warnings as errors", does not have any
     effect.


To disable a specific restriction check, use `-RRestrictions' gnatcheck
option with the corresponding restriction name as a parameter. `-R' is
not available for `Style_Checks' and `Warnings' options, to disable
warnings and style checks, use the corresponding warning and style
options.

   Note that if `Warnings' or `Warnings' rule is activated, this also
activates a default compiler warnings that do not correspond to any
specific parameter of warning control option, and the corresponding
diagnoses are included in the `gnatcheck' report file. You may disable
these diagnoses by using rule exemption mechanism (to do this, you
should create the corresponding exemption sections for `Warnings' rule).

6 Project-Wide Checks
*********************

In order to perform checks on all units of a given project, you can use
the GNAT driver along with the `-P' option:
        gnat check -Pproj -rules -from=my_rules

If the project `proj' depends upon other projects, you can perform
checks on the project closure using the `-U' option:
        gnat check -Pproj -U -rules -from=my_rules

Finally, if not all the units are relevant to a particular main program
in the project closure, you can perform checks for the set of units
needed to create a given main program (unit closure) using the `-U'
option followed by the name of the main unit:
        gnat check -Pproj -U main -rules -from=my_rules

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.

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

7.2 `gnatcheck' Annotations Rules
=================================

   * An "Exempt_Off" annotation can only appear after a corresponding
     "Exempt_On" annotation.

   * Exempted source code sections are only based on the source
     location of the annotations. Any source construct between the two
     annotations is part of the exempted source code section.

   * Exempted source code sections for different rules are independent.
     They can be nested or intersect with one another without
     limitation.  Creating nested or intersecting source code sections
     for the same rule is not allowed.

   * Malformed exempted source code sections are reported by a warning,
     and the corresponding rule exemptions are ignored.

   * When an exempted source code section does not contain at least one
     violation of the exempted rule, a warning is emitted on `stderr'.

   * If an "Exempt_On" annotation pragma does not have a matching
     "Exempt_Off" annotation pragma in the same compilation unit, then
     the exemption for the given rule is ignored and a warning is
     issued.

8 Predefined Rules
******************

The description of the rules currently implemented in `gnatcheck' is
given in this chapter.  The rule identifier is used as a parameter of
`gnatcheck''s `+R' or `-R' switches.

   Be aware that most of these rules apply to specialized coding
requirements developed by individual users and may well not make sense
in other environments. In particular, there are many rules that conflict
with one another. Proper usage of gnatcheck involves selecting the rules
you wish to apply by looking at your independently developed coding
standards and finding the corresponding gnatcheck rules.

8.1 Style-Related Rules
=======================

The rules in this section may be used to enforce various feature usages
consistent with good software engineering, for example as described in
`Ada 95 Quality and Style'.

8.1.1 Tasking
-------------

The rules in this subsection may be used to enforce various feature
usages related to concurrency.

8.1.1.1 `Multiple_Entries_In_Protected_Definitions'
...................................................

Flag each protected definition (i.e., each protected object/type
declaration) that defines more than one entry.  Diagnostic messages are
generated for all the entry declarations except the first one. An entry
family is counted as one entry. Entries from the private part of the
protected definition are also checked.

   This rule has no parameters.

8.1.1.2 `Volatile_Objects_Without_Address_Clauses'
..................................................

Flag each volatile object that does not have an address clause.

   The following check is made: if the pragma `Volatile' is applied to a
data object or to its type, then an address clause must be supplied for
this object.

   This rule does not check the components of data objects, array
components that are volatile as a result of the pragma
`Volatile_Components', or objects that are volatile because they are
atomic as a result of pragmas `Atomic' or `Atomic_Components'.

   Only variable declarations, and not constant declarations, are
checked.

   This rule has no parameters.

8.1.2 Object Orientation
------------------------

The rules in this subsection may be used to enforce various feature
usages related to Object-Oriented Programming.

8.1.2.1 `Deep_Inheritance_Hierarchies'
......................................

Flags a tagged derived type declaration or an interface type
declaration if its depth (in its inheritance hierarchy) exceeds the
value specified by the `N' rule parameter.

   The inheritance depth of a tagged type or interface type is defined
as 0 for a type  with no parent and no progenitor, and otherwise as 1 +
max of the depths of the immediate parent and immediate progenitors.

   This rule does not flag private extension declarations. In the case
of a private extension, the corresponding full declaration is checked.

   This rule has the following (mandatory) parameter for the `+R'
option:

_N_
     Integer not less than -1 specifying the maximal allowed depth of
     any inheritance hierarchy. If the rule parameter is set to -1, the
     rule flags all the declarations of tagged and interface types.

8.1.2.2 `Direct_Calls_To_Primitives'
....................................

Flags any non-dispatching call to a dispatching primitive operation,
except for two cases:

   * the common idiom where a primitive subprogram for a tagged type
     directly calls the same primitive subprogram of the type's
     immediate ancestor;

   * the type for that the called operation is a primitive operation is
     declared as private non tagged type (with the full view tagged),
     and at the place of the call the full declaration of the type is
     not visible;


   This rule has no parameters.

8.1.2.3 `Too_Many_Parents'
..........................

Flags any type declaration, single task declaration or single protected
declaration that has more then  `N' parents,  `N' is a parameter of the
rule.  A parent here is either a (sub)type denoted by the subtype mark
from the parent_subtype_indication (in case of a derived type
declaration), or any of the progenitors from the interface list, if any.

   This rule has the following (mandatory) parameters for the `+R'
option:

_N_
     Positive integer specifying the maximal allowed number of parents.

8.1.2.4 `Visible_Components'
............................

Flags all the type declarations located in the visible part of a library
package or a library generic package that can declare a visible
component. A type is considered as declaring a visible component if it
contains a record definition by its own or as a part of a record
extension. Type declaration is flagged even if it contains a record
definition that defines no components.

   Declarations located in private parts of local (generic) packages
are not flagged. Declarations in private packages are not flagged.

   This rule has no parameters.

8.1.3 Portability
-----------------

The rules in this subsection may be used to enforce various feature
usages that support program portability.

8.1.3.1 `Forbidden_Attributes'
..............................

Flag each use of the specified attributes. The attributes to be
detected are named in the rule's parameters.

   This rule has the following parameters:

   * For the `+R' option

    _Attribute_Designator_
          Adds the specified attribute to the set of attributes to be
          detected and sets the detection checks for all the specified
          attributes ON.  If _Attribute_Designator_ does not denote any
          attribute defined in the Ada standard or in *note
          Implementation Defined Attributes: (gnat_rm)Implementation
          Defined Attributes, it is treated as the name of unknown
          attribute.

    `GNAT'
          All the GNAT-specific attributes are detected; this sets the
          detection checks for all the specified attributes ON.

    `ALL'
          All attributes are detected; this sets the rule ON.

   * For the `-R' option
    _Attribute_Designator_
          Removes the specified attribute from the set of attributes to
          be detected without affecting detection checks for other
          attributes. If _Attribute_Designator_ does not correspond to
          any attribute defined in the Ada standard or in *note
          Implementation Defined Attributes: (gnat_rm)Implementation
          Defined Attributes, this option is treated as turning OFF
          detection of all unknown attributes.

    GNAT
          Turn OFF detection of all GNAT-specific attributes

    ALL
          Clear the list of the attributes to be detected and turn the
          rule OFF.

Parameters are not case sensitive. If _Attribute_Designator_ does not
have the syntax of an Ada identifier and therefore can not be
considered as a (part of an) attribute designator, a diagnostic message
is generated and the corresponding parameter is ignored. (If an
attribute allows a static expression to be a part of the attribute
designator, this expression is ignored by this rule.)

   When more then one parameter is given in the same rule option, the
parameters must be separated by commas.

   If more then one option for this rule is specified for the gnatcheck
call, a new option overrides the previous one(s).

   The `+R' option with no parameters turns the rule ON, with the set of
attributes to be detected defined by the previous rule options.  (By
default this set is empty, so if the only option specified for the rule
is `+RForbidden_Attributes' (with no parameter), then the rule is
enabled, but it does not detect anything).  The `-R' option with no
parameter turns the rule OFF, but it does not affect the set of
attributes to be detected.

8.1.3.2 `Forbidden_Pragmas'
...........................

Flag each use of the specified pragmas.  The pragmas to be detected are
named in the rule's  parameters.

   This rule has the following parameters:

   * For the `+R' option

    _Pragma_Name_
          Adds the specified pragma to the set of pragmas to be checked
          and sets the checks for all the specified pragmas ON.
          _Pragma_Name_ is treated as a name of a pragma. If it does
          not correspond to any pragma name defined in the Ada standard
          or to the name of a GNAT-specific pragma defined in *note
          Implementation Defined Pragmas: (gnat_rm)Implementation
          Defined Pragmas, it is treated as the name of unknown pragma.

    `GNAT'
          All the GNAT-specific pragmas are detected; this sets the
          checks for all the specified pragmas ON.

    `ALL'
          All pragmas are detected; this sets the rule ON.

   * For the `-R' option
    _Pragma_Name_
          Removes the specified pragma from the set of pragmas to be
          checked without affecting checks for other pragmas.
          _Pragma_Name_ is treated as a name of a pragma. If it does
          not correspond to any pragma defined in the Ada standard or
          to any name defined in *note Implementation Defined Pragmas:
          (gnat_rm)Implementation Defined Pragmas, this option is
          treated as turning OFF detection of all unknown pragmas.

    GNAT
          Turn OFF detection of all GNAT-specific pragmas

    ALL
          Clear the list of the pragmas to be detected and turn the
          rule OFF.

Parameters are not case sensitive. If _Pragma_Name_ does not have the
syntax of an Ada identifier and therefore can not be considered as a
pragma name, a diagnostic message is generated and the corresponding
parameter is ignored.

   When more then one parameter is given in the same rule option, the
parameters must be separated by a comma.

   If more then one option for this rule is specified for the
`gnatcheck' call, a new option overrides the previous one(s).

   The `+R' option with no parameters turns the rule ON with the set of
pragmas to be detected defined by the previous rule options.  (By
default this set is empty, so if the only option specified for the rule
is `+RForbidden_Pragmas' (with no parameter), then the rule is enabled,
but it does not detect anything).  The `-R' option with no parameter
turns the rule OFF, but it does not affect the set of pragmas to be
detected.

8.1.3.3 `Implicit_SMALL_For_Fixed_Point_Types'
..............................................

Flag each fixed point type declaration that lacks an explicit
representation  clause to define its `'Small' value.  Since `'Small'
can be  defined only for ordinary fixed point types, decimal fixed
point type declarations are not checked.

   This rule has no parameters.

8.1.3.4 `Predefined_Numeric_Types'
..................................

Flag each explicit use of the name of any numeric type or subtype
defined in package `Standard'.

   The rationale for this rule is to detect when the program may depend
on platform-specific characteristics of the implementation of the
predefined numeric types. Note that this rule is over-pessimistic; for
example, a program that uses `String' indexing likely needs a variable
of type `Integer'.  Another example is the flagging of predefined
numeric types with explicit constraints:

         subtype My_Integer is Integer range Left .. Right;
         Vy_Var : My_Integer;

This rule detects only numeric types and subtypes defined in
`Standard'. The use of numeric types and subtypes defined in other
predefined packages (such as `System.Any_Priority' or
`Ada.Text_IO.Count') is not flagged

   This rule has no parameters.

8.1.3.5 `Separate_Numeric_Error_Handlers'
.........................................

Flags each exception handler that contains a choice for the predefined
`Constraint_Error' exception, but does not contain the choice for the
predefined `Numeric_Error' exception, or that contains the choice for
`Numeric_Error', but does not contain the choice for `Constraint_Error'.

   This rule has no parameters.

8.1.4 Program Structure
-----------------------

The rules in this subsection may be used to enforce feature usages
related to program structure.

8.1.4.1 `Deeply_Nested_Generics'
................................

Flags a generic declaration nested in another generic declaration if
the nesting level of the inner generic exceeds a value specified by the
`N' rule parameter.  The nesting level is the number of generic
declarations that enclose the given (generic) declaration. Formal
packages are not flagged by this rule.

   This rule has the following (mandatory) parameters for the `+R'
option:

_N_
     Positive integer specifying the maximal allowed nesting level for
     a generic declaration.

8.1.4.2 `Local_Packages'
........................

Flag all local packages declared in package and generic package specs.
Local packages in bodies are not flagged.

   This rule has no parameters.

8.1.4.3 `Non_Visible_Exceptions'
................................

Flag constructs leading to the possibility of propagating an exception
out of the scope in which the exception is declared.  Two cases are
detected:

   * An exception declaration in a subprogram body, task body or block
     statement is flagged if the body or statement does not contain a
     handler for that exception or a handler with an `others' choice.

   * A `raise' statement in an exception handler of a subprogram body,
     task body or block statement is flagged if it (re)raises a locally
     declared exception.  This may occur under the following
     circumstances:
        - it explicitly raises a locally declared exception, or

        - it does not specify an exception name (i.e., it is simply
          `raise;') and the enclosing handler contains a locally
          declared exception in its exception choices.

Renamings of local exceptions are not flagged.

   This rule has no parameters.

8.1.4.4 `Raising_External_Exceptions'
.....................................

Flag any `raise' statement, in a program unit declared in a library
package or in a generic library package, for an exception that is
neither a predefined exception nor an exception that is also declared
(or renamed) in the visible part of the package.

   This rule has no parameters.

8.1.5 Programming Practice
--------------------------

The rules in this subsection may be used to enforce feature usages that
relate to program maintainability.

8.1.5.1 `Anonymous_Arrays'
..........................

Flag all anonymous array type definitions (by Ada semantics these can
only occur in object declarations).

   This rule has no parameters.

8.1.5.2 `Enumeration_Ranges_In_CASE_Statements'
...............................................

Flag each use of a range of enumeration literals as a choice in a
`case' statement.  All forms for specifying a range (explicit ranges
such as `A .. B', subtype marks and `'Range' attributes) are flagged.
An enumeration range is flagged even if contains exactly one
enumeration value or no values at all. A type derived from an
enumeration type is considered as an enumeration type.

   This rule helps prevent maintenance problems arising from adding an
enumeration value to a type and having it implicitly handled by an
existing `case' statement with an enumeration range that includes the
new literal.

   This rule has no parameters.

8.1.5.3 `Exceptions_As_Control_Flow'
....................................

Flag each place where an exception is explicitly raised and handled in
the same subprogram body. A `raise' statement in an exception handler,
package body, task body or entry body is not flagged.

   The rule has no parameters.

8.1.5.4 `Exits_From_Conditional_Loops'
......................................

Flag any exit statement if it transfers the control out of a `for' loop
or a `while' loop. This includes cases when the `exit' statement
applies to a `FOR' or `while' loop, and cases when it is enclosed in
some `for' or `while' loop, but transfers the control from some outer
(unconditional) `loop' statement.

   The rule has no parameters.

8.1.5.5 `EXIT_Statements_With_No_Loop_Name'
...........................................

Flag each `exit' statement that does not specify the name of the loop
being exited.

   The rule has no parameters.

8.1.5.6 `GOTO_Statements'
.........................

Flag each occurrence of a `goto' statement.

   This rule has no parameters.

8.1.5.7 `Improper_Returns'
..........................

Flag each explicit `return' statement in procedures, and multiple
`return' statements in functions.  Diagnostic messages are generated
for all `return' statements in a procedure (thus each procedure must be
written so that it returns implicitly at the end of its statement part),
and for all `return' statements in a function after the first one.
This rule supports the stylistic convention that each subprogram should
have no more than one point of normal return.

   This rule has no parameters.

8.1.5.8 `Non_Short_Circuit_Operators'
.....................................

Flag all calls to predefined `and' and `or' operators for any boolean
type. Calls to user-defined `and' and `or' and to operators defined by
renaming declarations are not flagged. Calls to predefined `and' and
`or' operators for modular types or boolean array types are not flagged.

   This rule has no parameters.

8.1.5.9 `OTHERS_In_Aggregates'
..............................

Flag each use of an `others' choice in extension aggregates.  In record
and array aggregates, an `others' choice is flagged unless it is used
to refer to all components, or to all but one component.

   If, in case of a named array aggregate, there are two associations,
one with an `others' choice and another with a discrete range, the
`others' choice is flagged even if the discrete range specifies exactly
one component; for example, `(1..1 => 0, others => 1)'.

   This rule has no parameters.

8.1.5.10 `OTHERS_In_CASE_Statements'
....................................

Flag any use of an `others' choice in a `case' statement.

   This rule has no parameters.

8.1.5.11 `OTHERS_In_Exception_Handlers'
.......................................

Flag any use of an `others' choice in an exception handler.

   This rule has no parameters.

8.1.5.12 `Overly_Nested_Control_Structures'
...........................................

Flag each control structure whose nesting level exceeds the value
provided in the rule parameter.

   The control structures checked are the following:

   * `if' statement

   * `case' statement

   * `loop' statement

   * Selective accept statement

   * Timed entry call statement

   * Conditional entry call

   * Asynchronous select statement

The rule has the following parameter for the `+R' option:

_N_
     Positive integer specifying the maximal control structure nesting
     level that is not flagged

If the parameter for the `+R' option is not specified or if it is not a
positive integer, `+R' option is ignored.

   If more then one  option is specified for the gnatcheck call, the
later option and new parameter override the previous one(s).

8.1.5.13 `Positional_Actuals_For_Defaulted_Generic_Parameters'
..............................................................

Flag each generic actual parameter corresponding to a generic formal
parameter with a default initialization, if positional notation is used.

   This rule has no parameters.

8.1.5.14 `Positional_Actuals_For_Defaulted_Parameters'
......................................................

Flag each actual parameter to a subprogram or entry call where the
corresponding formal parameter has a default expression, if positional
notation is used.

   This rule has no parameters.

8.1.5.15 `Positional_Components'
................................

Flag each array, record and extension aggregate that includes positional
notation.

   This rule has no parameters.

8.1.5.16 `Positional_Generic_Parameters'
........................................

Flag each positional actual generic parameter except for the case when
the generic unit being instantiated has exactly one generic formal
parameter.

   This rule has no parameters.

8.1.5.17 `Positional_Parameters'
................................

Flag each positional parameter notation in a subprogram or entry call,
except for the following:

   * Parameters of calls to of prefix or infix operators are not flagged

   * If the called subprogram or entry has only one formal parameter,
     the parameter of the call is not flagged;

   * If a subprogram call uses the _Object.Operation_ notation, then
        - the first parameter (that is, _Object_) is not flagged;

        - if the called subprogram has only two parameters, the second
          parameter of the call is not flagged;

This rule has no parameters.

8.1.5.18 `Recursive_Subprograms'
................................

Flags specs (and bodies that act as specs) of recursive subprograms. A
subprogram is considered as recursive in a given context if there exists
a chain of direct calls starting from the body of, and ending at this
subprogram within this context. A context is provided by the set of Ada
sources specified as arguments of a given gnatcheck call.  Neither
dispatching calls nor calls through access-to-subprograms are
considered as direct calls by this rule.

   Generic subprograms and subprograms detected in generic units are not
flagged. Recursive subprograms in expanded generic instantiations are
flagged.

   This rule has no parameters.

8.1.5.19 `Unconditional_Exits'
..............................

Flag unconditional `exit' statements.

   This rule has no parameters.

8.1.5.20 `Unnamed_Blocks_And_Loops'
...................................

Flag each unnamed block statement and loop statement.

   The rule has no parameters.

8.1.5.21 `USE_PACKAGE_Clauses'
..............................

Flag all `use' clauses for packages; `use type' clauses are not flagged.

   This rule has no parameters.

8.1.6 Readability
-----------------

The rules described in this subsection may be used to enforce feature
usages that contribute towards readability.

8.1.6.1 `Misnamed_Controlling_Parameters'
.........................................

Flags a declaration of a dispatching operation, if the first parameter
is not a controlling one and its name is not `This' (the check for
parameter name is not case-sensitive). Declarations of dispatching
functions with controlling result and no controlling parameter are
never flagged.

   A subprogram body declaration, subprogram renaming declaration or
subprogram body stub is flagged only if it is not a completion of a
prior subprogram declaration.

   This rule has no parameters.

8.1.6.2 `Misnamed_Identifiers'
..............................

Flag the declaration of each identifier that does not have a suffix
corresponding to the kind of entity being declared.  The following
declarations are checked:

   * type declarations

   * subtype declarations

   * constant declarations (but not number declarations)

   * package renaming declarations (but not generic package renaming
     declarations)

This rule may have parameters. When used without parameters, the rule
enforces the following checks:

   * type-defining names end with `_T', unless the type is an access
     type, in which case the suffix must be `_A'

   * constant names end with `_C'

   * names defining package renamings end with `_R'

Defining identifiers from incomplete type declarations are never
flagged.

   For a private type declaration (including private extensions), the
defining identifier from the private type declaration is checked
against the type suffix (even if the corresponding full declaration is
an access type declaration), and the defining identifier from the
corresponding full type declaration is not checked.

For a deferred constant, the defining name in the corresponding full
constant declaration is not checked.

   Defining names of formal types are not checked.

   The rule may have the following parameters:

   * For the `+R' option:
    `Default'
          Sets the default listed above for all the names to be checked.

    `Type_Suffix=_string_'
          Specifies the suffix for a type name.

    `Access_Suffix=_string_'
          Specifies the suffix for an access type name. If this
          parameter is set, it overrides for access types the suffix
          set by the `Type_Suffix' parameter.  For access types,
          _string_ may have the following format: _suffix1(suffix2)_.
          That means that an access type name should have the _suffix1_
          suffix except for the case when the designated type is also
          an access type, in this case the type name should have the
          _suffix1 & suffix2_ suffix.

    `Class_Access_Suffix=_string_'
          Specifies the suffix for the name of an access type that
          points to some class-wide type.  If this parameter is set, it
          overrides for such access types the suffix set by the
          `Type_Suffix' or `Access_Suffix' parameter.

    `Class_Subtype_Suffix=_string_'
          Specifies the suffix for the name of a subtype that denotes a
          class-wide type.

    `Constant_Suffix=_string_'
          Specifies the suffix for a constant name.

    `Renaming_Suffix=_string_'
          Specifies the suffix for a package renaming name.

   * For the `-R' option:
    `All_Suffixes'
          Remove all the suffixes specified for the identifier suffix
          checks, whether by default or as specified by other rule
          parameters. All the checks for this rule are disabled as a
          result.

    `Type_Suffix'
          Removes the suffix specified for types. This disables checks
          for types but does not disable any other checks for this rule
          (including the check for access type names if `Access_Suffix'
          is set).

    `Access_Suffix'
          Removes the suffix specified for access types.  This disables
          checks for access type names but does not disable any other
          checks for this rule.  If `Type_Suffix' is set, access type
          names are checked as ordinary type names.

    `Class_Access_Suffix'
          Removes the suffix specified for access types pointing to
          class-wide type. This disables specific checks for names of
          access types pointing to class-wide types but does not
          disable any other checks for this rule.  If `Type_Suffix' is
          set, access type names are checked as ordinary type names. If
          `Access_Suffix' is set, these access types are checked as any
          other access type name.

    `Class_Subtype_Suffix=_string_'
          Removes the suffix specified for subtype names.  This
          disables checks for subtype names but does not disable any
          other checks for this rule.

    `Constant_Suffix'
          Removes the suffix specified for constants. This disables
          checks for constant names but does not disable any other
          checks for this rule.

    `Renaming_Suffix'
          Removes the suffix specified for package renamings. This
          disables checks for package renamings but does not disable
          any other checks for this rule.

If more than one parameter is used, parameters must be separated by
commas.

   If more than one  option is specified for the `gnatcheck' invocation,
a new option overrides the previous one(s).

   The `+RMisnamed_Identifiers' option (with no parameter) enables
checks for all the name suffixes specified by previous options used for
this rule.

   The `-RMisnamed_Identifiers' option (with no parameter) disables all
the checks but keeps all the suffixes specified by previous options
used for this rule.

   The _string_ value must be a valid suffix for an Ada identifier
(after trimming all the leading and trailing space characters, if any).
Parameters are not case sensitive, except the _string_ part.

   If any error is detected in a rule parameter, the parameter is
ignored.  In such a case the options that are set for the rule are not
specified.

8.1.6.3 `Name_Clashes'
......................

Check that certain names are not used as defining identifiers. To
activate this rule, you need to supply a reference to the dictionary
file(s) as a rule parameter(s) (more then one dictionary file can be
specified). If no dictionary file is set, this rule will not cause
anything to be flagged.  Only defining occurrences, not references, are
checked.  The check is not case-sensitive.

   This rule is enabled by default, but without setting any
corresponding dictionary file(s); thus the default effect is to do no
checks.

   A dictionary file is a plain text file. The maximum line length for
this file is 1024 characters.  If the line is longer then this limit,
extra characters are ignored.

   Each line can be either an empty line, a comment line, or a line
containing a list of identifiers separated by space or HT characters.
A comment is an Ada-style comment (from `--' to end-of-line).
Identifiers must follow the Ada syntax for identifiers.  A line
containing one or more identifiers may end with a comment.

8.1.6.4 `Uncommented_BEGIN_In_Package_Bodies'
.............................................

Flags each package body with declarations and a statement part that
does not include a trailing comment on the line containing the `begin'
keyword; this trailing comment needs to specify the package name and
nothing else.  The `begin' is not flagged if the package body does not
contain any declarations.

   If the `begin' keyword is placed on the same line as the last
declaration or the first statement, it is flagged independently of
whether the line contains a trailing comment. The diagnostic message is
attached to the line containing the first statement.

   This rule has no parameters.

8.1.7 Source Code Presentation
------------------------------

This subsection is a placeholder; there are currently no rules in this
category.

8.2 Feature Usage Rules
=======================

The rules in this section can be used to enforce specific usage
patterns for a variety of language features.

8.2.1 `Abstract_Type_Declarations'
----------------------------------

Flag all declarations of abstract types. For an abstract private type,
both the private and full type declarations are flagged.

   This rule has no parameters.

8.2.2 `Anonymous_Subtypes'
--------------------------

Flag all uses of anonymous subtypes (except cases when subtype
indication is a part of a record component definition, and this subtype
indication depends on a discriminant). A use of an anonymous subtype is
any instance of a subtype indication with a constraint, other than one
that occurs immediately within a subtype declaration. Any use of a range
other than as a constraint used immediately within a subtype declaration
is considered as an anonymous subtype.

   An effect of this rule is that `for' loops such as the following are
flagged (since `1..N' is formally a "range"):

     for I in 1 .. N loop
        ...
     end loop;

Declaring an explicit subtype solves the problem:

     subtype S is Integer range 1..N;
     ...
     for I in S loop
        ...
     end loop;

This rule has no parameters.

8.2.3 `Blocks'
--------------

Flag each block statement.

   This rule has no parameters.

8.2.4 `Complex_Inlined_Subprograms'
-----------------------------------

Flags a subprogram (or generic subprogram) if pragma Inline is applied
to the subprogram and at least one of the following conditions is met:

   * it contains at least one complex declaration such as a subprogram
     body, package, task, protected declaration, or a generic
     instantiation (except instantiation of `Ada.Unchecked_Conversion');

   * it contains at least one complex statement such as a loop, a case
     or a if statement, or a short circuit control form;

   * the number of statements exceeds a value specified by the `N' rule
     parameter;

This rule has the following (mandatory) parameter for the `+R' option:

_N_
     Positive integer specifying the maximum allowed total number of
     statements in the subprogram body.

8.2.5 `Controlled_Type_Declarations'
------------------------------------

Flag all declarations of controlled types. A declaration of a private
type is flagged if its full declaration declares a controlled type. A
declaration of a derived type is flagged if its ancestor type is
controlled. Subtype declarations are not checked. A declaration of a
type that itself is not a descendant of a type declared in
`Ada.Finalization' but has a controlled component is not checked.

   This rule has no parameters.

8.2.6 `Declarations_In_Blocks'
------------------------------

Flag all block statements containing local declarations. A `declare'
block with an empty declarative_part or with a declarative part
containing only pragmas and/or `use' clauses is not flagged.

   This rule has no parameters.

8.2.7 `Deeply_Nested_Inlining'
------------------------------

Flags a subprogram (or generic subprogram) if pragma Inline has been
applied to the subprogram but the subprogram calls to another inlined
subprogram that results in nested inlining with nesting depth exceeding
the value specified by the `N' rule parameter.

   This rule requires the global analysis of all the compilation units
that are `gnatcheck' arguments; such analysis may affect the tool's
performance.

   This rule has the following (mandatory) parameter for the `+R'
option:

_N_
     Positive integer specifying the maximal allowed level of nested
     inlining.

8.2.8 `Default_Parameters'
--------------------------

Flag all default expressions in parameters specifications. All parameter
specifications are checked: in subprograms (including formal, generic
and protected subprograms) and in task and protected entries (including
accept statements and entry bodies).

   This rule has no parameters.

8.2.9 `Discriminated_Records'
-----------------------------

Flag all declarations of record types with discriminants. Only the
declarations of record and record extension types are checked.
Incomplete, formal, private, derived and private extension type
declarations are not checked. Task and protected type declarations also
are not checked.

   This rule has no parameters.

8.2.10 `Explicit_Full_Discrete_Ranges'
--------------------------------------

Flag each discrete range that has the form `A'First .. A'Last'.

   This rule has no parameters.

8.2.11 `Float_Equality_Checks'
------------------------------

Flag all calls to the predefined equality operations for floating-point
types.  Both "`='" and "`/='" operations are checked.  User-defined
equality operations are not flagged, nor are "`='" and "`/='"
operations for fixed-point types.

   This rule has no parameters.

8.2.12 `Function_Style_Procedures'
----------------------------------

Flag each procedure that can be rewritten as a function. A procedure
can be converted into a function if it has exactly one parameter of
mode `out' and no parameters of mode `in out'. Procedure declarations,
formal procedure declarations, and generic procedure declarations are
always checked. Procedure bodies and body stubs are flagged only if
they do not have corresponding separate declarations. Procedure
renamings and procedure instantiations are not flagged.

   If a procedure can be rewritten as a function, but its `out'
parameter is of a limited type, it is not flagged.

   Protected procedures are not flagged. Null procedures also are not
flagged.

   This rule has no parameters.

8.2.13 `Generics_In_Subprograms'
--------------------------------

Flag each declaration of a generic unit in a subprogram. Generic
declarations in the bodies of generic subprograms are also flagged.  A
generic unit nested in another generic unit is not flagged.  If a
generic unit is declared in a local package that is declared in a
subprogram body, the generic unit is flagged.

   This rule has no parameters.

8.2.14 `Implicit_IN_Mode_Parameters'
------------------------------------

Flag each occurrence of a formal parameter with an implicit `in' mode.
Note that `access' parameters, although they technically behave like
`in' parameters, are not flagged.

   This rule has no parameters.

8.2.15 `Improperly_Located_Instantiations'
------------------------------------------

Flag all generic instantiations in library-level package specs
(including library generic packages) and in all subprogram bodies.

   Instantiations in task and entry bodies are not flagged.
Instantiations in the bodies of protected subprograms are flagged.

   This rule has no parameters.

8.2.16 `Library_Level_Subprograms'
----------------------------------

Flag all library-level subprograms (including generic subprogram
instantiations).

   This rule has no parameters.

8.2.17 `Non_Qualified_Aggregates'
---------------------------------

Flag each non-qualified aggregate.  A non-qualified aggregate is an
aggregate that is not the expression of a qualified expression. A
string literal is not considered an aggregate, but an array aggregate
of a string type is considered as a normal aggregate.  Aggregates of
anonymous array types are not flagged.

   This rule has no parameters.

8.2.18 `Numeric_Literals'
-------------------------

Flag each use of a numeric literal in an index expression, and in any
circumstance except for the following:

   * a literal occurring in the initialization expression for a constant
     declaration or a named number declaration, or

   * an integer literal that is less than or equal to a value specified
     by the `N' rule parameter.

   * a literal occurring in a declaration in case the `Statements_Only'
     rule parameter is given

This rule may have the following parameters for the `+R' option:

_N_
     _N_ is an integer literal used as the maximal value that is not
     flagged (i.e., integer literals not exceeding this value are
     allowed)

`ALL'
     All integer literals are flagged

`Statements_Only'
     Numeric literals are flagged only when used in statements

If no parameters are set, the maximum unflagged value is 1, and the
check for literals is not limited by statements only.

   The last specified check limit (or the fact that there is no limit at
all) is used when multiple `+R' options appear.

   The `-R' option for this rule has no parameters.  It disables the
rule and restores its default operation mode.  If the `+R' option
subsequently appears, will be 1, and the check will not be limited by
statements only.

8.2.19 `Parameters_Out_Of_Order'
--------------------------------

Flag each subprogram and entry declaration whose formal parameters are
not ordered according to the following scheme:

   * `in' and `access' parameters first, then `in out' parameters, and
     then `out' parameters;

   * for `in' mode, parameters with default initialization expressions
     occur last

Only the first violation of the described order is flagged.

   The following constructs are checked:

   * subprogram declarations (including null procedures);

   * generic subprogram declarations;

   * formal subprogram declarations;

   * entry declarations;

   * subprogram bodies and subprogram body stubs that do not have
     separate specifications

Subprogram renamings are not checked.

   This rule has no parameters.

8.2.20 `Raising_Predefined_Exceptions'
--------------------------------------

Flag each `raise' statement that raises a predefined exception (i.e.,
one of the exceptions `Constraint_Error', `Numeric_Error',
`Program_Error', `Storage_Error', or `Tasking_Error').

   This rule has no parameters.

8.2.21 `Unassigned_OUT_Parameters'
----------------------------------

Flags procedures' `out' parameters that are not assigned, and
identifies the contexts in which the assignments are missing.

   An `out' parameter is flagged in the statements in the procedure
body's handled sequence of statements (before the procedure body's
`exception' part, if any) if this sequence of statements contains no
assignments to the parameter.

   An `out' parameter is flagged in an exception handler in the
exception part of the procedure body's handled sequence of statements
if the handler contains neither assignment to the parameter nor a
`raise' statement.

   Bodies of generic procedures are also considered.

   The following are treated as assignments to an `out' parameter:

   * an assignment statement, with the parameter or some component as
     the target;

   * passing the parameter (or one of its components) as an `out' or
     `in out' parameter.

This rule does not have any parameters.

8.2.22 `Unconstrained_Array_Returns'
------------------------------------

Flag each function returning an unconstrained array. Function
declarations, function bodies (and body stubs) having no separate
specifications, and generic function instantiations are checked.
Function calls and function renamings are not checked.

   Generic function declarations, and function declarations in generic
packages are not checked, instead this rule checks the results of
generic instantiations (that is, expanded specification and expanded
body corresponding to an instantiation).

   This rule has the following (optional) parameters for the `+R'
option:

_Except_String_
     Do not flag functions that return the predefined `String' type or
     a type derived from it, directly or indirectly.

8.3 Metrics-Related Rules
=========================

The rules in this section can be used to enforce compliance with
specific code metrics, by checking that the metrics computed for a
program lie within user-specifiable bounds.  Depending on the metric,
there may be a lower bound, an upper bound, or both.  A construct is
flagged if the value of the metric exceeds the upper bound or is less
than the lower bound.

   The name of any metrics rule consists of the prefix `Metrics_'
followed by the name of the corresponding metric:
`Essential_Complexity', `Cyclomatic_Complexity', or `LSLOC'.  (The
"LSLOC" acronym stands for "Logical Source Lines Of Code".)  The
meaning and the computed values of the metrics are the same as in
`gnatmetric'.

   For the `+R' option, each metrics rule has a numeric parameter
specifying the bound (integer or real, depending on a metric).  The `-R'
option for the metrics rules does not have a parameter.

_Example:_ the rule
     +RMetrics_Cyclomatic_Complexity : 7
   means that all bodies with cyclomatic complexity exceeding 7 will be
flagged.

   To turn OFF the check for cyclomatic complexity metric, use the
following option:
     -RMetrics_Cyclomatic_Complexity

8.3.1 `Metrics_Essential_Complexity'
------------------------------------

The `Metrics_Essential_Complexity' rule takes a positive integer as
upper bound.  A construct exceeding this limit will be flagged.

8.3.2 `Metrics_Cyclomatic_Complexity'
-------------------------------------

The `Metrics_Cyclomatic_Complexity' rule takes a positive integer as
upper bound.  A construct exceeding this limit will be flagged.

8.3.3 `Metrics_LSLOC'
---------------------

The `Metrics_LSLOC' rule takes a positive integer as upper bound.  A
compilation unit exceeding this limit will be flagged.

8.4 SPARK Ada Rules
===================

The rules in this section can be used to enforce compliance with the
Ada subset allowed by the SPARK tools.

8.4.1 `Annotated_Comments'
--------------------------

Flags comments that are used as annotations or as special
sentinels/markers. Such comments have the following structure

       --<special_character> <comment_marker>

where

`<special_character>'
     character (such as '#', '$', '|' etc.) indicating that the comment
     is used for a specific purpose

`<comment_marker>'
     a word identifying the annotation or special usage (word here is
     any sequence of characters except white space)

There may be any amount of white space (including none at all) between
`<special_character>' and `<comment_marker>', but no white space is
permitted between `'--'' and `<special_character>'. (A white space here
is either a space character or horizontal tabulation)

   `<comment_marker>' must not contain any white space.

   `<comment_marker>' may be empty, in which case the rule flags each
comment that starts with `--<special_character>' and that does not
contain any other character except white space

   The rule has the following (mandatory) parameter for the `+R' option:

_S_
     String with the following interpretation: the first character is
     the special comment character, and the rest is the comment marker.
     S must not contain white space.

The `-R' option erases all definitions of special comment annotations
specified by the previous +R options.

   The rule is case-sensitive.

   Example:

   The rule

   +R
     Annotated_Comments:#hide

will flag the following comment lines

   +R
     --#hide
     --# hide
     --#           hide

        I := I + 1; --# hide

But the line

   +R
     -- # hide

will not be flagged, because of the space between '-' and '#'.

   The line

   +R
     --#Hide

will not be flagged, because the string parameter is case sensitive.

8.4.2 `Boolean_Relational_Operators'
------------------------------------

Flag each call to a predefined relational operator ("<", ">", "<=",
">=", "=" and "/=") for the predefined Boolean type.  (This rule is
useful in enforcing the SPARK language restrictions.)

   Calls to predefined relational operators of any type derived from
`Standard.Boolean' are not detected.  Calls to user-defined functions
with these designators, and uses of operators that are renamings of the
predefined relational operators for `Standard.Boolean', are likewise
not detected.

   This rule has no parameters.

8.4.3 `Expanded_Loop_Exit_Names'
--------------------------------

Flag all expanded loop names in `exit' statements.

   This rule has no parameters.

8.4.4 `Non_SPARK_Attributes'
----------------------------

The SPARK language defines the following subset of Ada 95 attribute
designators as those that can be used in SPARK programs. The use of any
other attribute is flagged.

   * `'Adjacent'

   * `'Aft'

   * `'Base'

   * `'Ceiling'

   * `'Component_Size'

   * `'Compose'

   * `'Copy_Sign'

   * `'Delta'

   * `'Denorm'

   * `'Digits'

   * `'Exponent'

   * `'First'

   * `'Floor'

   * `'Fore'

   * `'Fraction'

   * `'Last'

   * `'Leading_Part'

   * `'Length'

   * `'Machine'

   * `'Machine_Emax'

   * `'Machine_Emin'

   * `'Machine_Mantissa'

   * `'Machine_Overflows'

   * `'Machine_Radix'

   * `'Machine_Rounds'

   * `'Max'

   * `'Min'

   * `'Model'

   * `'Model_Emin'

   * `'Model_Epsilon'

   * `'Model_Mantissa'

   * `'Model_Small'

   * `'Modulus'

   * `'Pos'

   * `'Pred'

   * `'Range'

   * `'Remainder'

   * `'Rounding'

   * `'Safe_First'

   * `'Safe_Last'

   * `'Scaling'

   * `'Signed_Zeros'

   * `'Size'

   * `'Small'

   * `'Succ'

   * `'Truncation'

   * `'Unbiased_Rounding'

   * `'Val'

   * `'Valid'

This rule has no parameters.

8.4.5 `Non_Tagged_Derived_Types'
--------------------------------

Flag all derived type declarations that do not have a record extension
part.

   This rule has no parameters.

8.4.6 `Outer_Loop_Exits'
------------------------

Flag each `exit' statement containing a loop name that is not the name
of the immediately enclosing `loop' statement.

   This rule has no parameters.

8.4.7 `Overloaded_Operators'
----------------------------

Flag each function declaration that overloads an operator symbol.  A
function body is checked only if the body does not have a separate
spec. Formal functions are also checked. For a renaming declaration,
only renaming-as-declaration is checked

   This rule has no parameters.

8.4.8 `Slices'
--------------

Flag all uses of array slicing

   This rule has no parameters.

8.4.9 `Universal_Ranges'
------------------------

Flag discrete ranges that are a part of an index constraint, constrained
array definition, or `for'-loop parameter specification, and whose
bounds are both of type universal_integer. Ranges that have at least one
bound of a specific type (such as `1 .. N', where `N' is a variable or
an expression of non-universal type) are not flagged.

   This rule has no parameters.

9 Example of `gnatcheck' Usage
******************************

Here is a simple example. Suppose that in the current directory we have
a project file named `gnatcheck_example.gpr' with the following content:

     project Gnatcheck_Example is

        for Source_Dirs use ("src");
        for Object_Dir use "obj";
        for Main use ("main.adb");

        package Check is
           for Default_Switches ("ada") use ("-rules", "-from=coding_standard");
        end Check;

     end Gnatcheck_Example;

And the file named `coding_standard' is also located in the current
directory and has the following content:

     -----------------------------------------------------
     -- This is a sample gnatcheck coding standard file --
     -----------------------------------------------------

     --  First, turning on rules, that are directly implemented in gnatcheck
     +RAbstract_Type_Declarations
     +RAnonymous_Arrays
     +RLocal_Packages
     +RFloat_Equality_Checks
     +REXIT_Statements_With_No_Loop_Name

     --  Then, activating compiler checks of interest:
     +RStyle_Checks:e
     --  This style check checks if a unit name is present on END keyword that
     --  is the end of the unit declaration

And the subdirectory `src' contains the following Ada sources:

   `pack.ads':

     package Pack is
        type T is abstract tagged private;
        procedure P (X : T) is abstract;

        package Inner is
           type My_Float is digits 8;
           function Is_Equal (L, R : My_Float) return Boolean;
        end Inner;
     private
        type T is abstract tagged null record;
     end;

`pack.adb':

     package body Pack is
        package body Inner is
           function Is_Equal (L, R : My_Float) return Boolean is
           begin
              return L = R;
           end;
        end Inner;
     end Pack;

and `main.adb'

     with Pack; use Pack;
     procedure Main is

        pragma Annotate
          (gnatcheck, Exempt_On, "Anonymous_Arrays", "this one is fine");
        Float_Array : array (1 .. 10) of Inner.My_Float;
        pragma Annotate (gnatcheck, Exempt_Off, "Anonymous_Arrays");

        Another_Float_Array : array (1 .. 10) of Inner.My_Float;

        use Inner;

        B : Boolean := False;

     begin
        for J in Float_Array'Range loop
           if Is_Equal (Float_Array (J), Another_Float_Array (J)) then
              B := True;
              exit;
           end if;
        end loop;
     end Main;

And suppose we call `gnatcheck' from the current directory using the
`gnat' driver:

        gnat check -Pgnatcheck_example.gpr

As a result, `gnatcheck' is called to check all the files from the
project `gnatcheck_example.gpr' using the coding standard defined by
the file `coding_standard'. As the result, the `gnatcheck' report file
named `gnatcheck.out' will be created in the current directory, and it
will have the following content:

     RULE CHECKING REPORT

     1. OVERVIEW

     Date and time of execution: 2009.10.28 14:17
     Tool version: GNATCHECK (built with ASIS 2.0.R for GNAT Pro 6.3.0w (20091016))
     Command line:

     gnatcheck -files=.../GNAT-TEMP-000004.TMP -cargs -gnatec=.../GNAT-TEMP-000003.TMP -rules -from=coding_standard

     Coding standard (applied rules):
        Abstract_Type_Declarations
        Anonymous_Arrays
        EXIT_Statements_With_No_Loop_Name
        Float_Equality_Checks
        Local_Packages

        Compiler style checks: -gnatye

     Number of coding standard violations: 6
     Number of exempted coding standard violations: 1

     2. DETECTED RULE VIOLATIONS

     2.1. NON-EXEMPTED VIOLATIONS

     Source files with non-exempted violations
        pack.ads
        pack.adb
        main.adb

     List of violations grouped by files, and ordered by increasing source location:

     pack.ads:2:4: declaration of abstract type
     pack.ads:5:4: declaration of local package
     pack.ads:10:30: declaration of abstract type
     pack.ads:11:1: (style) "end Pack" required
     pack.adb:5:19: use of equality operation for float values
     pack.adb:6:7: (style) "end Is_Equal" required
     main.adb:9:26: anonymous array type
     main.adb:19:10: exit statement with no loop name

     2.2. EXEMPTED VIOLATIONS

     Source files with exempted violations
        main.adb

     List of violations grouped by files, and ordered by increasing source location:

     main.adb:6:18: anonymous array type
        (this one is fine)

     2.3. SOURCE FILES WITH NO VIOLATION

        No files without violations

     END OF REPORT

Appendix A List of Rules
************************

This Appendix contains an alphabetized list of all the predefined
GNATcheck rules.

   * `Abstract_Type_Declarations'
     *Note Abstract_Type_Declarations::.

   * `Anonymous_Arrays'
     *Note Anonymous_Arrays::.

   * `Anonymous_Subtypes'
     *Note Anonymous_Subtypes::.

   * `Blocks'
     *Note Blocks::.

   * `Boolean_Relational_Operators'
     *Note Boolean_Relational_Operators::.

   * `Complex_Inlined_Subprograms'
     *Note Complex_Inlined_Subprograms::.

   * `Controlled_Type_Declarations'
     *Note Controlled_Type_Declarations::.

   * `Declarations_In_Blocks'
     *Note Declarations_In_Blocks::.

   * `Deep_Inheritance_Hierarchies'
     *Note Deep_Inheritance_Hierarchies::.

   * `Deeply_Nested_Generics'
     *Note Deeply_Nested_Generics::.

   * `Deeply_Nested_Inlining'
     *Note Deeply_Nested_Inlining::.

   * `Default_Parameters'
     *Note Default_Parameters::.

   * `Direct_Calls_To_Primitives'
     *Note Direct_Calls_To_Primitives::.

   * `Discriminated_Records'
     *Note Discriminated_Records::.

   * `Enumeration_Ranges_In_CASE_Statements'
     *Note Enumeration_Ranges_In_CASE_Statements::.

   * `Exceptions_As_Control_Flow'
     *Note Exceptions_As_Control_Flow::.

   * `Exits_From_Conditional_Loops'
     *Note Exits_From_Conditional_Loops::.

   * `EXIT_Statements_With_No_Loop_Name'
     *Note EXIT_Statements_With_No_Loop_Name::.

   * `Expanded_Loop_Exit_Names'
     *Note Expanded_Loop_Exit_Names::.

   * `Explicit_Full_Discrete_Ranges'
     *Note Explicit_Full_Discrete_Ranges::.

   * `Float_Equality_Checks'
     *Note Float_Equality_Checks::.

   * `Forbidden_Attributes'
     *Note Forbidden_Attributes::.

   * `Forbidden_Pragmas'
     *Note Forbidden_Pragmas::.

   * `Function_Style_Procedures'
     *Note Function_Style_Procedures::.

   * `Generics_In_Subprograms'
     *Note Generics_In_Subprograms::.

   * `GOTO_Statements'
     *Note GOTO_Statements::.

   * `Implicit_IN_Mode_Parameters'
     *Note Implicit_IN_Mode_Parameters::.

   * `Implicit_SMALL_For_Fixed_Point_Types'
     *Note Implicit_SMALL_For_Fixed_Point_Types::.

   * `Improperly_Located_Instantiations'
     *Note Improperly_Located_Instantiations::.

   * `Improper_Returns'
     *Note Improper_Returns::.

   * `Library_Level_Subprograms'
     *Note Library_Level_Subprograms::.

   * `Local_Packages'
     *Note Local_Packages::.

   * `Metrics_Cyclomatic_Complexity'
     *Note Metrics_Cyclomatic_Complexity::.

   * `Metrics_Essential_Complexity'
     *Note Metrics_Essential_Complexity::.

   * `Metrics_LSLOC'
     *Note Metrics_LSLOC::.

   * `Misnamed_Controlling_Parameters'
     *Note Misnamed_Controlling_Parameters::.

   * `Misnamed_Identifiers'
     *Note Misnamed_Identifiers::.

   * `Multiple_Entries_In_Protected_Definitions'
     *Note Multiple_Entries_In_Protected_Definitions::.

   * `Name_Clashes'
     *Note Name_Clashes::.

   * `Non_Qualified_Aggregates'
     *Note Non_Qualified_Aggregates::.

   * `Non_Short_Circuit_Operators'
     *Note Non_Short_Circuit_Operators::.

   * `Non_SPARK_Attributes'
     *Note Non_SPARK_Attributes::.

   * `Non_Tagged_Derived_Types'
     *Note Non_Tagged_Derived_Types::.

   * `Non_Visible_Exceptions'
     *Note Non_Visible_Exceptions::.

   * `Numeric_Literals'
     *Note Numeric_Literals::.

   * `OTHERS_In_Aggregates'
     *Note OTHERS_In_Aggregates::.

   * `OTHERS_In_CASE_Statements'
     *Note OTHERS_In_CASE_Statements::.

   * `OTHERS_In_Exception_Handlers'
     *Note OTHERS_In_Exception_Handlers::.

   * `Outer_Loop_Exits'
     *Note Outer_Loop_Exits::.

   * `Overloaded_Operators'
     *Note Overloaded_Operators::.

   * `Overly_Nested_Control_Structures'
     *Note Overly_Nested_Control_Structures::.

   * `Parameters_Out_Of_Order'
     *Note Parameters_Out_Of_Order::.

   * `Positional_Actuals_For_Defaulted_Generic_Parameters'
     *Note Positional_Actuals_For_Defaulted_Generic_Parameters::.

   * `Positional_Actuals_For_Defaulted_Parameters'
     *Note Positional_Actuals_For_Defaulted_Parameters::.

   * `Positional_Components'
     *Note Positional_Components::.

   * `Positional_Generic_Parameters'
     *Note Positional_Generic_Parameters::.

   * `Positional_Parameters'
     *Note Positional_Parameters::.

   * `Predefined_Numeric_Types'
     *Note Predefined_Numeric_Types::.

   * `Raising_External_Exceptions'
     *Note Raising_External_Exceptions::.

   * `Raising_Predefined_Exceptions'
     *Note Raising_Predefined_Exceptions::.

   * `Separate_Numeric_Error_Handlers'
     *Note Separate_Numeric_Error_Handlers::.

   * `Slices'
     *Note Slices::.

   * `Too_Many_Parents'
     *Note Too_Many_Parents::.

   * `Unassigned_OUT_Parameters'
     *Note Unassigned_OUT_Parameters::.

   * `Uncommented_BEGIN_In_Package_Bodies'
     *Note Uncommented_BEGIN_In_Package_Bodies::.

   * `Recursive_Subprograms'
     *Note Recursive_Subprograms::.

   * `Unconditional_Exits'
     *Note Unconditional_Exits::.

   * `Unconstrained_Array_Returns'
     *Note Unconstrained_Array_Returns::.

   * `Universal_Ranges'
     *Note Universal_Ranges::.

   * `Unnamed_Blocks_And_Loops'
     *Note Unnamed_Blocks_And_Loops::.

   * `USE_PACKAGE_Clauses'
     *Note USE_PACKAGE_Clauses::.

   * `Visible_Components'
     *Note Visible_Components::.

   * `Volatile_Objects_Without_Address_Clauses'
     *Note Volatile_Objects_Without_Address_Clauses::.


Appendix B GNU Free Documentation License
*****************************************

Version 1.1, March 2000

Copyright (C) 2000 Free Software Foundation, Inc.
59 Temple Place, Suite 330, Boston, MA  02111-1307  USA

Everyone is permitted to copy and distribute verbatim copies of this
license document, but changing it is not allowed.

0. PREAMBLE
===========

The purpose of this License is to make a manual, textbook, or other
written document "free" in the sense of freedom: to assure everyone the
effective freedom to copy and redistribute it, with or without
modifying it, either commercially or noncommercially.  Secondarily,
this License preserves for the author and publisher a way to get credit
for their work, while not being considered responsible for
modifications made by others.

   This License is a kind of "copyleft", which means that derivative
works of the document must themselves be free in the same sense.  It
complements the GNU General Public License, which is a copyleft license
designed for free software.

   We have designed this License in order to use it for manuals for free
software, because free software needs free documentation: a free
program should come with manuals providing the same freedoms that the
software does.  But this License is not limited to software manuals; it
can be used for any textual work, regardless of subject matter or
whether it is published as a printed book.  We recommend this License
principally for works whose purpose is instruction or reference.

1. APPLICABILITY AND DEFINITIONS
================================

This License applies to any manual or other work that contains a notice
placed by the copyright holder saying it can be distributed under the
terms of this License.  The "Document", below, refers to any such
manual or work.  Any member of the public is a licensee, and is
addressed as "you".

   A "Modified Version" of the Document means any work containing the
Document or a portion of it, either copied verbatim, or with
modifications and/or translated into another language.

   A "Secondary Section" is a named appendix or a front-matter section
of the Document that deals exclusively with the relationship of the
publishers or authors of the Document to the Document's overall subject
(or to related matters) and contains nothing that could fall directly
within that overall subject.  (For example, if the Document is in part a
textbook of mathematics, a Secondary Section may not explain any
mathematics.)  The relationship could be a matter of historical
connection with the subject or with related matters, or of legal,
commercial, philosophical, ethical or political position regarding them.

   The "Invariant Sections" are certain Secondary Sections whose titles
are designated, as being those of Invariant Sections, in the notice
that says that the Document is released under this License.

   The "Cover Texts" are certain short passages of text that are listed,
as Front-Cover Texts or Back-Cover Texts, in the notice that says that
the Document is released under this License.

   A "Transparent" copy of the Document means a machine-readable copy,
represented in a format whose specification is available to the general
public, whose contents can be viewed and edited directly and
straightforwardly with generic text editors or (for images composed of
pixels) generic paint programs or (for drawings) some widely available
drawing editor, and that is suitable for input to text formatters or
for automatic translation to a variety of formats suitable for input to
text formatters.  A copy made in an otherwise Transparent file format
whose markup has been designed to thwart or discourage subsequent
modification by readers is not Transparent.  A copy that is not
"Transparent" is called "Opaque".

   Examples of suitable formats for Transparent copies include plain
ASCII without markup, Texinfo input format, LaTeX input format, SGML or
XML using a publicly available DTD, and standard-conforming simple HTML
designed for human modification.  Opaque formats include PostScript,
PDF, proprietary formats that can be read and edited only by
proprietary word processors, SGML or XML for which the DTD and/or
processing tools are not generally available, and the machine-generated
HTML produced by some word processors for output purposes only.

   The "Title Page" means, for a printed book, the title page itself,
plus such following pages as are needed to hold, legibly, the material
this License requires to appear in the title page.  For works in
formats which do not have any title page as such, "Title Page" means
the text near the most prominent appearance of the work's title,
preceding the beginning of the body of the text.

2. VERBATIM COPYING
===================

You may copy and distribute the Document in any medium, either
commercially or noncommercially, provided that this License, the
copyright notices, and the license notice saying this License applies
to the Document are reproduced in all copies, and that you add no other
conditions whatsoever to those of this License.  You may not use
technical measures to obstruct or control the reading or further
copying of the copies you make or distribute.  However, you may accept
compensation in exchange for copies.  If you distribute a large enough
number of copies you must also follow the conditions in section 3.

   You may also lend copies, under the same conditions stated above, and
you may publicly display copies.

3. COPYING IN QUANTITY
======================

If you publish printed copies of the Document numbering more than 100,
and the Document's license notice requires Cover Texts, you must enclose
the copies in covers that carry, clearly and legibly, all these Cover
Texts: Front-Cover Texts on the front cover, and Back-Cover Texts on
the back cover.  Both covers must also clearly and legibly identify you
as the publisher of these copies.  The front cover must present the
full title with all words of the title equally prominent and visible.
You may add other material on the covers in addition.  Copying with
changes limited to the covers, as long as they preserve the title of
the Document and satisfy these conditions, can be treated as verbatim
copying in other respects.

   If the required texts for either cover are too voluminous to fit
legibly, you should put the first ones listed (as many as fit
reasonably) on the actual cover, and continue the rest onto adjacent
pages.

   If you publish or distribute Opaque copies of the Document numbering
more than 100, you must either include a machine-readable Transparent
copy along with each Opaque copy, or state in or with each Opaque copy
a publicly-accessible computer-network location containing a complete
Transparent copy of the Document, free of added material, which the
general network-using public has access to download anonymously at no
charge using public-standard network protocols.  If you use the latter
option, you must take reasonably prudent steps, when you begin
distribution of Opaque copies in quantity, to ensure that this
Transparent copy will remain thus accessible at the stated location
until at least one year after the last time you distribute an Opaque
copy (directly or through your agents or retailers) of that edition to
the public.

   It is requested, but not required, that you contact the authors of
the Document well before redistributing any large number of copies, to
give them a chance to provide you with an updated version of the
Document.

4. MODIFICATIONS
================

You may copy and distribute a Modified Version of the Document under
the conditions of sections 2 and 3 above, provided that you release the
Modified Version under precisely this License, with the Modified
Version filling the role of the Document, thus licensing distribution
and modification of the Modified Version to whoever possesses a copy of
it.  In addition, you must do these things in the Modified Version:
  A. Use in the Title Page (and on the covers, if any) a title distinct
       from that of the Document, and from those of previous versions
     (which should, if there were any, be listed in the History section
       of the Document).  You may use the same title as a previous
     version    if the original publisher of that version gives
     permission.

  B. List on the Title Page, as authors, one or more persons or entities
       responsible for authorship of the modifications in the Modified
      Version, together with at least five of the principal authors of
     the    Document (all of its principal authors, if it has less than
     five).

  C. State on the Title page the name of the publisher of the
     Modified Version, as the publisher.

  D. Preserve all the copyright notices of the Document.

  E. Add an appropriate copyright notice for your modifications
     adjacent to the other copyright notices.

  F. Include, immediately after the copyright notices, a license notice
       giving the public permission to use the Modified Version under
     the    terms of this License, in the form shown in the Addendum
     below.

  G. Preserve in that license notice the full lists of Invariant
     Sections    and required Cover Texts given in the Document's
     license notice.

  H. Include an unaltered copy of this License.

  I. Preserve the section entitled "History", and its title, and add to
       it an item stating at least the title, year, new authors, and
     publisher of the Modified Version as given on the Title Page.  If
      there is no section entitled "History" in the Document, create one
       stating the title, year, authors, and publisher of the Document
     as    given on its Title Page, then add an item describing the
     Modified    Version as stated in the previous sentence.

  J. Preserve the network location, if any, given in the Document for
     public access to a Transparent copy of the Document, and likewise
      the network locations given in the Document for previous versions
       it was based on.  These may be placed in the "History" section.
       You may omit a network location for a work that was published at
       least four years before the Document itself, or if the original
      publisher of the version it refers to gives permission.

  K. In any section entitled "Acknowledgements" or "Dedications",
     preserve the section's title, and preserve in the section all the
      substance and tone of each of the contributor acknowledgements
     and/or dedications given therein.

  L. Preserve all the Invariant Sections of the Document,    unaltered
     in their text and in their titles.  Section numbers    or the
     equivalent are not considered part of the section titles.

  M. Delete any section entitled "Endorsements".  Such a section    may
     not be included in the Modified Version.

  N. Do not retitle any existing section as "Endorsements"    or to
     conflict in title with any Invariant Section.

   If the Modified Version includes new front-matter sections or
appendices that qualify as Secondary Sections and contain no material
copied from the Document, you may at your option designate some or all
of these sections as invariant.  To do this, add their titles to the
list of Invariant Sections in the Modified Version's license notice.
These titles must be distinct from any other section titles.

   You may add a section entitled "Endorsements", provided it contains
nothing but endorsements of your Modified Version by various parties -
for example, statements of peer review or that the text has been
approved by an organization as the authoritative definition of a
standard.

   You may add a passage of up to five words as a Front-Cover Text, and
a passage of up to 25 words as a Back-Cover Text, to the end of the list
of Cover Texts in the Modified Version.  Only one passage of
Front-Cover Text and one of Back-Cover Text may be added by (or through
arrangements made by) any one entity.  If the Document already includes
a cover text for the same cover, previously added by you or by
arrangement made by the same entity you are acting on behalf of, you
may not add another; but you may replace the old one, on explicit
permission from the previous publisher that added the old one.

   The author(s) and publisher(s) of the Document do not by this License
give permission to use their names for publicity for or to assert or
imply endorsement of any Modified Version.

5. COMBINING DOCUMENTS
======================

You may combine the Document with other documents released under this
License, under the terms defined in section 4 above for modified
versions, provided that you include in the combination all of the
Invariant Sections of all of the original documents, unmodified, and
list them all as Invariant Sections of your combined work in its
license notice.

   The combined work need only contain one copy of this License, and
multiple identical Invariant Sections may be replaced with a single
copy.  If there are multiple Invariant Sections with the same name but
different contents, make the title of each such section unique by
adding at the end of it, in parentheses, the name of the original
author or publisher of that section if known, or else a unique number.
Make the same adjustment to the section titles in the list of Invariant
Sections in the license notice of the combined work.

   In the combination, you must combine any sections entitled "History"
in the various original documents, forming one section entitled
"History"; likewise combine any sections entitled "Acknowledgements",
and any sections entitled "Dedications".  You must delete all sections
entitled "Endorsements."

   Heading 6. COLLECTIONS OF DOCUMENTS

   You may make a collection consisting of the Document and other
documents released under this License, and replace the individual
copies of this License in the various documents with a single copy that
is included in the collection, provided that you follow the rules of
this License for verbatim copying of each of the documents in all other
respects.

   You may extract a single document from such a collection, and
distribute it individually under this License, provided you insert a
copy of this License into the extracted document, and follow this
License in all other respects regarding verbatim copying of that
document.

7. AGGREGATION WITH INDEPENDENT WORKS
=====================================

A compilation of the Document or its derivatives with other separate
and independent documents or works, in or on a volume of a storage or
distribution medium, does not as a whole count as a Modified Version of
the Document, provided no compilation copyright is claimed for the
compilation.  Such a compilation is called an "aggregate", and this
License does not apply to the other self-contained works thus compiled
with the Document, on account of their being thus compiled, if they are
not themselves derivative works of the Document.

   If the Cover Text requirement of section 3 is applicable to these
copies of the Document, then if the Document is less than one quarter
of the entire aggregate, the Document's Cover Texts may be placed on
covers that surround only the Document within the aggregate.  Otherwise
they must appear on covers around the whole aggregate.

8. TRANSLATION
==============

Translation is considered a kind of modification, so you may distribute
translations of the Document under the terms of section 4.  Replacing
Invariant Sections with translations requires special permission from
their copyright holders, but you may include translations of some or
all Invariant Sections in addition to the original versions of these
Invariant Sections.  You may include a translation of this License
provided that you also include the original English version of this
License.  In case of a disagreement between the translation and the
original English version of this License, the original English version
will prevail.

9. TERMINATION
==============

You may not copy, modify, sublicense, or distribute the Document except
as expressly provided for under this License.  Any other attempt to
copy, modify, sublicense or distribute the Document is void, and will
automatically terminate your rights under this License.  However,
parties who have received copies, or rights, from you under this
License will not have their licenses terminated so long as such parties
remain in full compliance.

10. FUTURE REVISIONS OF THIS LICENSE
====================================

The Free Software Foundation may publish new, revised versions of the
GNU Free Documentation License from time to time.  Such new versions
will be similar in spirit to the present version, but may differ in
detail to address new problems or concerns.  See
http://www.gnu.org/copyleft/.

   Each version of the License is given a distinguishing version number.
If the Document specifies that a particular numbered version of this
License "or any later version" applies to it, you have the option of
following the terms and conditions either of that specified version or
of any later version that has been published (not as a draft) by the
Free Software Foundation.  If the Document does not specify a version
number of this License, you may choose any version ever published (not
as a draft) by the Free Software Foundation.

ADDENDUM: How to use this License for your documents
====================================================

To use this License in a document you have written, include a copy of
the License in the document and put the following copyright and license
notices just after the title page:

     Copyright (c)  YEAR  YOUR NAME.
     Permission is granted to copy, distribute and/or modify this
     document under the terms of the GNU Free Documentation License,
     Version 1.1 or any later version published by the Free Software
     Foundation; with the Invariant Sections being LIST THEIR TITLES,
     with the Front-Cover Texts being LIST, and with the Back-Cover
     Texts being LIST.  A copy of the license is included in the
     section entitled "GNU Free Documentation License".

   If you have no Invariant Sections, write "with no Invariant Sections"
instead of saying which ones are invariant.  If you have no Front-Cover
Texts, write "no Front-Cover Texts" instead of "Front-Cover Texts being
LIST"; likewise for Back-Cover Texts.

   If your document contains nontrivial examples of program code, we
recommend releasing these examples in parallel under your choice of
free software license, such as the GNU General Public License, to
permit their use in free software.

Index
*****

+R (gnatcheck):                                See 4.        (line  232)
--include-file=FILE:                           See 3.        (line  204)
--write-rules:                                 See 3.        (line  217)
-a:                                            See 3.        (line  162)
-ALL (gnatcheck):                              See 4.        (line  229)
-d:                                            See 3.        (line  166)
-from (gnatcheck):                             See 4.        (line  245)
-h:                                            See 3.        (line  175)
-l:                                            See 3.        (line  178)
-log:                                          See 3.        (line  184)
-m:                                            See 3.        (line  189)
-o:                                            See 3.        (line  214)
-q:                                            See 3.        (line  195)
-R (gnatcheck):                                See 4.        (line  241)
-s:                                            See 3.        (line  200)
-t:                                            See 3.        (line  207)
-v:                                            See 3.        (line  210)
Abstract_Type_Declarations:                    See 8.2.1.    (line 1256)
Annotated_Comments:                            See 8.4.1.    (line 1649)
Anonymous_Arrays:                              See 8.1.5.1.  (line  807)
Anonymous_Subtypes:                            See 8.2.2.    (line 1264)
ASIS:                                          See 1.        (line   82)
Blocks:                                        See 8.2.3.    (line 1292)
Boolean_Relational_Operators:                  See 8.4.2.    (line 1720)
Coding standard file (for gnatcheck):          See 4.        (line  258)
Complex_Inlined_Subprograms:                   See 8.2.4.    (line 1299)
Controlled_Type_Declarations:                  See 8.2.5.    (line 1321)
Declarations_In_Blocks:                        See 8.2.6.    (line 1333)
Deep_Inheritance_Hierarchies:                  See 8.1.2.1.  (line  491)
Deeply_Nested_Generics:                        See 8.1.4.1.  (line  742)
Deeply_Nested_Inlining:                        See 8.2.7.    (line 1342)
Default_Parameters:                            See 8.2.8.    (line 1361)
Direct_Calls_To_Primitives:                    See 8.1.2.2.  (line  513)
Discriminated_Records:                         See 8.2.9.    (line 1371)
Enumeration_Ranges_In_CASE_Statements:         See 8.1.5.2.  (line  815)
Exceptions_As_Control_Flow:                    See 8.1.5.3.  (line  832)
EXIT_Statements_With_No_Loop_Name:             See 8.1.5.5.  (line  852)
Exits_From_Conditional_Loops:                  See 8.1.5.4.  (line  841)
Expanded_Loop_Exit_Names:                      See 8.4.3.    (line 1735)
Explicit_Full_Discrete_Ranges:                 See 8.2.10.   (line 1382)
Feature usage related rules:                   See 8.2.      (line 1250)
Float_Equality_Checks:                         See 8.2.11.   (line 1389)
Forbidden_Attributes:                          See 8.1.3.1.  (line  567)
Forbidden_Pragmas:                             See 8.1.3.2.  (line  631)
Format of the Report File:                     See 2.        (line  133)
Free Documentation License, GNU:               See Appendix B.
                                                             (line 2277)
Function_Style_Procedures:                     See 8.2.12.   (line 1399)
Generics_In_Subprograms:                       See 8.2.13.   (line 1418)
gnatcheck annotations rules:                   See 7.2.      (line  402)
GNU Free Documentation License:                See Appendix B.
                                                             (line 2277)
GOTO_Statements:                               See 8.1.5.6.  (line  860)
Implicit_IN_Mode_Parameters:                   See 8.2.14.   (line 1429)
Implicit_SMALL_For_Fixed_Point_Types:          See 8.1.3.3.  (line  693)
Improper_Returns:                              See 8.1.5.7.  (line  867)
Improperly_Located_Instantiations:             See 8.2.15.   (line 1438)
Library_Level_Subprograms:                     See 8.2.16.   (line 1449)
License, GNU Free Documentation:               See Appendix B.
                                                             (line 2277)
Local_Packages:                                See 8.1.4.2.  (line  758)
Metrics-related rules:                         See 8.3.      (line 1595)
Metrics_Cyclomatic_Complexity:                 See 8.3.2.    (line 1631)
Metrics_Essential_Complexity:                  See 8.3.1.    (line 1625)
Metrics_LSLOC:                                 See 8.3.3.    (line 1637)
Misnamed_Controlling_Parameters:               See 8.1.6.1.  (line 1049)
Misnamed_Identifiers:                          See 8.1.6.2.  (line 1064)
Multiple_Entries_In_Protected_Definitions:     See 8.1.1.1.  (line  455)
Name_Clashes:                                  See 8.1.6.3.  (line 1204)
Non_Qualified_Aggregates:                      See 8.2.17.   (line 1457)
Non_Short_Circuit_Operators:                   See 8.1.5.8.  (line  880)
Non_SPARK_Attributes:                          See 8.4.4.    (line 1742)
Non_Tagged_Derived_Types:                      See 8.4.5.    (line 1849)
Non_Visible_Exceptions rule:                   See 8.1.4.3.  (line  766)
Numeric_Literals:                              See 8.2.18.   (line 1468)
Object-Orientation related rules:              See 8.1.2.    (line  485)
OTHERS_In_Aggregates:                          See 8.1.5.9.  (line  890)
OTHERS_In_CASE_Statements:                     See 8.1.5.10. (line  904)
OTHERS_In_Exception_Handlers:                  See 8.1.5.11. (line  911)
Outer_Loop_Exits:                              See 8.4.6.    (line 1857)
Overloaded_Operators:                          See 8.4.7.    (line 1865)
Overly_Nested_Control_Structures:              See 8.1.5.12. (line  918)
Parameters_Out_Of_Order:                       See 8.2.19.   (line 1507)
Portability-related rules:                     See 8.1.3.    (line  561)
Positional_Actuals_For_Defaulted_Generic_Parameters:See 8.1.5.13.
                                                             (line  952)
Positional_Actuals_For_Defaulted_Parameters rule:See 8.1.5.14.
                                                             (line  960)
Positional_Components:                         See 8.1.5.15. (line  969)
Positional_Generic_Parameters:                 See 8.1.5.16. (line  977)
Positional_Parameters:                         See 8.1.5.17. (line  986)
Predefined Rules:                              See 8.        (line  428)
Predefined_Numeric_Types:                      See 8.1.3.4.  (line  703)
Program Structure related rules:               See 8.1.4.    (line  736)
Programming Practice related rules:            See 8.1.5.    (line  801)
Project-Wide Checks:                           See 6.        (line  329)
Raising_External_Exceptions:                   See 8.1.4.4.  (line  791)
Raising_Predefined_Exceptions:                 See 8.2.20.   (line 1538)
Readability-related rules:                     See 8.1.6.    (line 1043)
Recursive_Subprograms rule:                    See 8.1.5.18. (line 1005)
Rule exemption:                                See 7.        (line  346)
Separate_Numeric_Error_Handlers:               See 8.1.3.5.  (line  726)
Slices:                                        See 8.4.8.    (line 1875)
Source code presentation related rules:        See 8.1.7.    (line 1244)
SPARK Ada related rules:                       See 8.4.      (line 1643)
Style-related rules:                           See 8.1.      (line  442)
Tasking-related rules:                         See 8.1.1.    (line  449)
Too_Many_Parents:                              See 8.1.2.3.  (line  531)
Unassigned_OUT_Parameters:                     See 8.2.21.   (line 1547)
Uncommented_BEGIN_In_Package_Bodies:           See 8.1.6.4.  (line 1228)
Unconditional_Exits rule:                      See 8.1.5.19. (line 1022)
Unconstrained_Array_Returns:                   See 8.2.22.   (line 1575)
Universal_Ranges rule:                         See 8.4.9.    (line 1882)
Unnamed_Blocks_And_Loops:                      See 8.1.5.20. (line 1029)
USE_PACKAGE_Clauses:                           See 8.1.5.21. (line 1036)
Using pragma Annotate to control rule exemption:See 7.1.     (line  367)
Visible_Components:                            See 8.1.2.4.  (line  546)
Volatile_Objects_Without_Address_Clauses:      See 8.1.1.2.  (line  466)
Table of Contents
*****************

GNATcheck Reference Manual
About This Manual
  What This Manual Contains
  What You Should Know Before Reading This Manual
1 Introduction
2 Format of the Report File
3 General `gnatcheck' Switches
4 `gnatcheck' Rule Options
5 Adding the Results of Compiler Checks to `gnatcheck' Output
6 Project-Wide Checks
7 Rule exemption
  7.1 Using pragma `Annotate' to Control Rule Exemption
  7.2 `gnatcheck' Annotations Rules
8 Predefined Rules
  8.1 Style-Related Rules
    8.1.1 Tasking
      8.1.1.1 `Multiple_Entries_In_Protected_Definitions'
      8.1.1.2 `Volatile_Objects_Without_Address_Clauses'
    8.1.2 Object Orientation
      8.1.2.1 `Deep_Inheritance_Hierarchies'
      8.1.2.2 `Direct_Calls_To_Primitives'
      8.1.2.3 `Too_Many_Parents'
      8.1.2.4 `Visible_Components'
    8.1.3 Portability
      8.1.3.1 `Forbidden_Attributes'
      8.1.3.2 `Forbidden_Pragmas'
      8.1.3.3 `Implicit_SMALL_For_Fixed_Point_Types'
      8.1.3.4 `Predefined_Numeric_Types'
      8.1.3.5 `Separate_Numeric_Error_Handlers'
    8.1.4 Program Structure
      8.1.4.1 `Deeply_Nested_Generics'
      8.1.4.2 `Local_Packages'
      8.1.4.3 `Non_Visible_Exceptions'
      8.1.4.4 `Raising_External_Exceptions'
    8.1.5 Programming Practice
      8.1.5.1 `Anonymous_Arrays'
      8.1.5.2 `Enumeration_Ranges_In_CASE_Statements'
      8.1.5.3 `Exceptions_As_Control_Flow'
      8.1.5.4 `Exits_From_Conditional_Loops'
      8.1.5.5 `EXIT_Statements_With_No_Loop_Name'
      8.1.5.6 `GOTO_Statements'
      8.1.5.7 `Improper_Returns'
      8.1.5.8 `Non_Short_Circuit_Operators'
      8.1.5.9 `OTHERS_In_Aggregates'
      8.1.5.10 `OTHERS_In_CASE_Statements'
      8.1.5.11 `OTHERS_In_Exception_Handlers'
      8.1.5.12 `Overly_Nested_Control_Structures'
      8.1.5.13 `Positional_Actuals_For_Defaulted_Generic_Parameters'
      8.1.5.14 `Positional_Actuals_For_Defaulted_Parameters'
      8.1.5.15 `Positional_Components'
      8.1.5.16 `Positional_Generic_Parameters'
      8.1.5.17 `Positional_Parameters'
      8.1.5.18 `Recursive_Subprograms'
      8.1.5.19 `Unconditional_Exits'
      8.1.5.20 `Unnamed_Blocks_And_Loops'
      8.1.5.21 `USE_PACKAGE_Clauses'
    8.1.6 Readability
      8.1.6.1 `Misnamed_Controlling_Parameters'
      8.1.6.2 `Misnamed_Identifiers'
      8.1.6.3 `Name_Clashes'
      8.1.6.4 `Uncommented_BEGIN_In_Package_Bodies'
    8.1.7 Source Code Presentation
  8.2 Feature Usage Rules
    8.2.1 `Abstract_Type_Declarations'
    8.2.2 `Anonymous_Subtypes'
    8.2.3 `Blocks'
    8.2.4 `Complex_Inlined_Subprograms'
    8.2.5 `Controlled_Type_Declarations'
    8.2.6 `Declarations_In_Blocks'
    8.2.7 `Deeply_Nested_Inlining'
    8.2.8 `Default_Parameters'
    8.2.9 `Discriminated_Records'
    8.2.10 `Explicit_Full_Discrete_Ranges'
    8.2.11 `Float_Equality_Checks'
    8.2.12 `Function_Style_Procedures'
    8.2.13 `Generics_In_Subprograms'
    8.2.14 `Implicit_IN_Mode_Parameters'
    8.2.15 `Improperly_Located_Instantiations'
    8.2.16 `Library_Level_Subprograms'
    8.2.17 `Non_Qualified_Aggregates'
    8.2.18 `Numeric_Literals'
    8.2.19 `Parameters_Out_Of_Order'
    8.2.20 `Raising_Predefined_Exceptions'
    8.2.21 `Unassigned_OUT_Parameters'
    8.2.22 `Unconstrained_Array_Returns'
  8.3 Metrics-Related Rules
    8.3.1 `Metrics_Essential_Complexity'
    8.3.2 `Metrics_Cyclomatic_Complexity'
    8.3.3 `Metrics_LSLOC'
  8.4 SPARK Ada Rules
    8.4.1 `Annotated_Comments'
    8.4.2 `Boolean_Relational_Operators'
    8.4.3 `Expanded_Loop_Exit_Names'
    8.4.4 `Non_SPARK_Attributes'
    8.4.5 `Non_Tagged_Derived_Types'
    8.4.6 `Outer_Loop_Exits'
    8.4.7 `Overloaded_Operators'
    8.4.8 `Slices'
    8.4.9 `Universal_Ranges'
9 Example of `gnatcheck' Usage
Appendix A List of Rules
Appendix B GNU Free Documentation License
Index


