\input texinfo   @c -*-texinfo-*-
@input texiplus

@c %**start of header

@c oooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooo
@c                                                                            o
@c                            GNAT DOCUMENTATION                              o
@c                                                                            o
@c                          G N A T C H E C K _ R M                           o
@c                                                                            o
@c                      Copyright (C) 2009-2011, AdaCore                      o
@c                                                                            o
@c  GNATCHECK  is  free  software;  you can  redistribute it and/or modify it o
@c  under  terms of  the GNU General Public License  as published by the Free o
@c  Software  Foundation;  either  version 2,  or (at your option)  any later o
@c  version.  GNAT  is  distributed  in the  hope that it will be useful, but o
@c  WITHOUT   ANY   WARRANTY;   without   even   the   implied   warranty  of o
@c  MERCHANTABILITY or FITNESS FOR A  PARTICULAR PURPOSE. See the GNU General o
@c  Public  License  for more  details.  You should have  received  a copy of o
@c  the  GNU  General Public License distributed with GNAT; see file COPYING. o
@c  If  not,  write  to  the   Free  Software Foundation, 51 Franklin Street, o
@c  Fifth Floor, Boston, MA 02110-1301, USA.                                  o
@c                                                                            o
@c  GNATCHECK is maintained by Ada Core Technologies Inc                      o
@c  (http://www.gnat.com).                                                    o
@c                                                                            o
@c oooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooo

@c oooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooo
@c
@c                           GNATCHECK_RM Style Guide
@c
@c  1. Always put a @noindent on the line before the first paragraph
@c     after any of these commands:
@c
@c          @chapter
@c          @section
@c          @subsection
@c          @subsubsection
@c          @subsubsubsection
@c
@c          @end smallexample
@c          @end itemize
@c          @end enumerate
@c
@c  2. DO NOT use @example. Use @smallexample instead.
@c
@c  3. Each @chapter, @section, @subsection, @subsubsection, etc.
@c     command must be preceded by two empty lines
@c
@c  4. The @item command must be on a line of its own if it is in an
@c     @itemize or @enumerate command.
@c
@c oooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooo

@setfilename gnatcheck_rm.info
@include version.texi

@set NOW December 2009
@c This flag is used where the text refers to conditions that exist when the
@c text was entered into the document but which may change over time.
@c Update the setting for the flag, and (if necessary) the text surrounding,
@c the references to the flag, on future doc revisions:
@c search for @value{NOW}.

@include edition.texi
@c edition.texi contains commands that set exactly one of the flags
@c FSFEDITION, PROEDITION, GPLEDITION
@c and that clear the other two

@ifset FSFEDITION
@set GNATEDITION GNAT
@end ifset

@ifset PROEDITION
@set GNATEDITION GNAT Pro
@end ifset

@ifset GPLEDITION
@set GNATEDITION GNAT
@end ifset


@settitle GNATcheck Reference Manual
@setchapternewpage odd
@syncodeindex fn cp
@c %**end of header

@titlepage

@title GNATcheck Reference Manual
@sp 1

@flushright
@titlefont{@i{Coding Standard Verifier}}
@end flushright
@sp 2

@ifset FSFEDITION
@subtitle GNAT, The GNU Ada Compiler
@subtitle GNAT Version @value{gnat_version}
@end ifset
@c ----------
@ifset PROEDITION
@subtitle The GNAT Pro Ada Compiler
@subtitle GNAT Pro Version @value{gnat_version}
@end ifset
@c ----------
@ifset GPLEDITION
@subtitle The GNAT Ada Compiler
@subtitle GNAT GPL Edition, Version @value{gnat_version}
@end ifset

@c ----------

@subtitle Configuration level: 180752
@subtitle Date: 2011/10/29

@author AdaCore

@page
@vskip 0pt plus 1filll

Copyright @copyright{} 2009-2011, 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''.

@end titlepage


@ifinfo
@node Top, About This Manual, (dir), (dir)
@top GNATcheck Reference Manual
@noindent
GNATcheck Reference Manual@*
Coding Standard Verifier
@sp 1

@noindent
@ifset FSFEDITION
GNAT, The GNU Ada Compiler@*
GNAT Version @value{gnat_version}@*
@end ifset
@c ----------
@ifset PROEDITION
The GNAT Pro Ada Compiler@*
GNAT Pro Version @value{gnat_version}@*
@end ifset
@c ----------
@ifset GPLEDITION
The GNAT Ada Compiler@*
GNAT GPL Edition, Version @value{gnat_version}@*
@end ifset
@c ----------
@noindent
Configuration level: 180752@*
Date: 2011/10/29

@noindent
Copyright @copyright{} 2009, AdaCore

@noindent
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''.

@menu
* About This Manual::
* Introduction::
* Format of the Report File::
* General gnatcheck Switches::
* gnatcheck Rule Options::
* Adding the Results of Compiler Checks to gnatcheck Output::
* Project-Wide Checks::
* Rule exemption::
* Predefined Rules::
* Example of gnatcheck Usage::
@ignore
* How to add a new rule
@end ignore
* List of Rules::
* GNU Free Documentation License::
* Index::

@detailmenu
 --- The Detailed Node Listing ---

About This Manual

* What This Manual Contains::
* What You Should Know Before Reading This Manual::

Introduction

Format of the Report File

General gnatcheck Switches

gnatcheck Rule Options

Adding the Results of Compiler Checks to gnatcheck Output

Project-Wide Checks

Rule exemption

* Using pragma Annotate to Control Rule Exemption::
* gnatcheck Annotations Rules::

Predefined Rules

* Style-Related Rules::
* Feature Usage Rules::
* Metrics-Related Rules::
* SPARK Ada Rules::

Example of gnatcheck Usage

List of Rules

GNU Free Documentation License

Index
@end detailmenu

@end menu
@end ifinfo

@c ********************
@node About This Manual
@c ********************
@unnumbered About This Manual


@noindent
The @command{gnatcheck} tool in @value{GNATEDITION} can be used to
enforce coding conventions by analyzing Ada source programs with respect to
a set of @i{rules} supplied at tool invocation.
This manual describes the complete set of predefined rules that
@command{gnatcheck} can take as input.

@menu
* What This Manual Contains::
* What You Should Know Before Reading This Manual::
@end menu

@node What This Manual Contains
@unnumberedsec What This Manual Contains

@noindent
This manual contains a description of @command{gnatcheck}, an ASIS-based
 utility that checks properties of Ada source files according to a given
 set of semantic rules

@itemize
@item

@ref{Introduction}, gives the general overview of the @command{gnatcheck}
tool

@ref{Format of the Report File}, describes the structure of the report file
generated by @command{gnatcheck}

@ref{General gnatcheck Switches}, describes switches control the general
@command{gnatcheck} behavior

@ref{gnatcheck Rule Options}, describes options used to control a set of
rules to be checked by @command{gnatcheck}

@ref{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 @command{gnatcheck}

@ref{Project-Wide Checks}, explains how to apply @command{gnatcheck} to
all the sources of your project

@ref{Rule exemption}, explains how to turn off a rule check for a specified
fragment of a source file

@ref{Predefined Rules}, contains a description of each predefined
@command{gnatcheck} rule, organized into categories.

@ref{Example of gnatcheck Usage}, contains a full example of
@command{gnatcheck} usage

@ref{List of Rules}, gives an alphabetized list of all predefined rules, for
ease of reference.
@end itemize

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


@node What You Should Know Before Reading This Manual
@unnumberedsec What You Should Know Before Reading This Manual

@noindent
You should be familiar with the Ada language and with the usage of
@value{GNATEDITION} in general;
please refer to the @cite{@value{GNATEDITION} User's Guide}.



@c ***********************
@node Introduction
@c ***********************
@chapter Introduction

@noindent
        The @command{gnatcheck} tool is an ASIS-based utility that checks properties
of Ada source files according to a given set of semantic rules.
@cindex ASIS

In order to check compliance with a given rule, @command{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 @command{gnatcheck}, either through a specified project file or
through @command{gnatcheck} switches as described below.

A number of rules are predefined in @command{gnatcheck} and are described
later in this chapter.
You can also add new rules, by modifying the @command{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 @command{gnatcheck} is provided by the GNAT
driver (see @cite{The GNAT Driver and Project Files} section in
@cite{@value{GNATEDITION} User's Guide}).


Invoking @command{gnatcheck} on the command line has the form:

@smallexample
@c $ gnatcheck @ovar{switches}  @{@var{filename}@}
@c       @r{[}-files=@{@var{arg_list_filename}@}@r{]}
@c       @r{[}-cargs @var{gcc_switches}@r{]} -rules @var{rule_options}
@c Expanding @ovar macro inline (explanation in macro def comments)
$ gnatcheck @r{[}@var{switches}@r{]}  @{@var{filename}@}
      @r{[}-files=@{@var{arg_list_filename}@}@r{]}
      @r{[}-cargs @var{gcc_switches}@r{]} -rules @var{rule_options}
@end smallexample

@noindent
where
@itemize @bullet
@item
@var{switches} specify the general tool options

@item
Each @var{filename} is the name (including the extension) of a source
file to process. ``Wildcards'' are allowed, and
the file name may contain path information.

@item
Each @var{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.

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

@item
@var{rule_options} is a list of options for controlling a set of
rules to be checked by @command{gnatcheck} (@pxref{gnatcheck Rule Options}).
@end itemize

@noindent
Either a @file{@var{filename}} or an @file{@var{arg_list_filename}} must be
supplied.

@c ***********************
@node Format of the Report File
@c ***********************
@chapter Format of the Report File
@cindex Format of the Report File

@noindent
The @command{gnatcheck} tool outputs on @file{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 @file{gnatcheck.out} and it is located in the
current directory; the @option{-o} option can be used to change the
name and/or location of the report file. This report contains:

@itemize @bullet

@item general details of the @command{gnatcheck} run: date and time of the run,
the version of the tool that has generated this report, full parameters
of the  @command{gnatcheck} invocation, reference to the list of checked
sources and applied rules (coding standard);
@item summary of the run (number of checked sources and detected violations);
@item list of exempted coding standard violations;
@item list of non-exempted coding standard violations;
@item list of problems in the definition of exemption sections;
@item list of language violations (compile-time errors) detected in processed sources;
@end itemize

@c ***********************
@node General gnatcheck Switches
@c ***********************
@chapter General @command{gnatcheck} Switches
@noindent
The following switches control the general @command{gnatcheck} behavior

@table @option
@c !sort!
@cindex @option{-a}
@item -a
Process all units including those with read-only ALI files such as
those from the GNAT Run-Time library.

@cindex @option{-d}
@item -d@var{x}
Activate internal debugging switches. @var{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 @code{ASIS_UL.Debug} unit in the ASIS Utility
Library source file @file{asis_ul-debug.adb}.

@cindex @option{-h}
@item -h
List all the rules checked by the given @command{gnatcheck} version.

@cindex @option{-l}
@item -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.

@cindex @option{-log}
@item -log
Duplicate all the output sent to @file{stderr} into a log file. The log file
is named @file{gnatcheck.log} and is located in the current directory.

@cindex @option{-m}
@item -m@i{nnnn}
Maximum number of diagnostics to be sent to @file{stdout}, where @i{nnnn} is in
the range 0@dots{}1000;
the default value is 500. Zero means that there is no limitation on
the number of diagnostic messages to be output.

@cindex @option{-q}
@item -q
Quiet mode. All the diagnostics about rule violations are placed in the
@command{gnatcheck} report file only, without duplication on @file{stdout}.

@cindex @option{-s}
@item -s
Short format of the report file (no version information, no list of applied
rules, no list of checked sources is included)

@cindex @option{--include-file=@var{file}}
@item --include-file=@var{file}
Append the content of the specified text file to the report file

@cindex @option{-t}
@item -t
Print out execution time.

@cindex @option{-v}
@item -v
Verbose mode; @command{gnatcheck} generates version information and then
a trace of sources being processed.

@cindex @option{-o}
@item -o @var{report_file}
Set name of report file file to @var{report_file} .

@cindex @option{--write-rules}
@item --write-rules=@var{template_file}
Write to @var{template_file} the template rule file that contains all the rules
currently implemented in @command{gnatcheck} turned off. A user may edit this
template file manually to get his own coding standard file.

@end table


@c ***********************
@node gnatcheck Rule Options
@c ***********************
@chapter @command{gnatcheck} Rule Options

@noindent
The following options control the processing performed by
@command{gnatcheck}.

@table @option
@cindex @option{-ALL} (@command{gnatcheck})
@item -ALL
Turn all the rule checks OFF.

@cindex @option{+R} (@command{gnatcheck})
@item +R@var{rule_id}@r{[}:@var{param}@r{]}
Turn on the check for a specified rule with the specified parameter, if any.
@var{rule_id} must be the identifier of one of the currently implemented rules
(use @option{-h} for the list of implemented rules). Rule identifiers
are not case-sensitive. The @var{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.

@cindex @option{-R} (@command{gnatcheck})
@item -R@var{rule_id}@r{[}:@var{param}@r{]}
Turn off the check for a specified rule with the specified parameter, if any.

@cindex @option{-from} (@command{gnatcheck})
@item -from=@var{rule_option_filename}
Read the rule options from the text file @var{rule_option_filename}, referred
to as a ``coding standard file'' below.

@end table

@noindent
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.
@cindex Coding standard file (for @code{gnatcheck})
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 @option{-from=@var{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, @file{@var{rule_file_1}} reads rule options
from @file{@var{rule_file_2}}, and @file{@var{rule_file_2}} reads
(directly or indirectly) rule options from @file{@var{rule_file_1}}),
processing fails with an error message.

@c ***********************
@node Adding the Results of Compiler Checks to gnatcheck Output
@c ***********************
@chapter Adding the Results of Compiler Checks to @command{gnatcheck} Output

@noindent
The @command{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 @option{+R} with
the following rule identifiers and parameters:

@table @option
@item Restrictions
To record restrictions violations (which are performed by the compiler if the
pragma @code{Restrictions} or @code{Restriction_Warnings} are given),
use the @code{Restrictions} rule
with the same parameters as pragma
@code{Restrictions} or @code{Restriction_Warnings}.

@item Style_Checks
To record compiler style checks
(see @cite{Style Checking} section in
@cite{@value{GNATEDITION} User's Guide}),
use the
@code{Style_Checks} rule.
This rule takes a parameter in one of the following forms:
@itemize
@item
@code{All_Checks},
which enables the standard style checks corresponding to the @option{-gnatyy}
GNAT style check option, or

@item
a string with the same
structure and semantics as the @code{string_LITERAL} parameter of the
GNAT pragma @code{Style_Checks}
(for further information about this pragma,
@pxref{Pragma Style_Checks,,, gnat_rm, GNAT Reference Manual}).
@end itemize

@noindent
For example, the
@code{+RStyle_Checks:O} rule option activates
the compiler style check that corresponds to
@code{-gnatyO} style check option.

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

@end table

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

Note that if @code{Warnings} or @code{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 @command{gnatcheck} report file. You may disable these diagnoses
by using rule exemption mechanism (to do this, you should create the
corresponding exemption sections for @code{Warnings} rule).




@c ***********************
@node Project-Wide Checks
@c ***********************
@chapter Project-Wide Checks
@cindex Project-Wide Checks

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

@noindent
If the project @code{proj} depends upon other projects, you can perform
checks on the project closure using the @option{-U} option:
@smallexample
   gnat check -Pproj -U -rules -from=my_rules
@end smallexample

@noindent
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 @option{-U} option followed by the name of the main unit:
@smallexample
   gnat check -Pproj -U main -rules -from=my_rules
@end smallexample



@c ***********************
@node Rule exemption
@c ***********************
@chapter Rule exemption
@cindex Rule exemption

@noindent
One of the most useful applications of @command{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 @command{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 @file{stderr}
and in a report file. In contrast, exempted violations are not listed on
@file{stderr}; thus users invoking @command{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
@command{gnatcheck} generates.

@menu
* Using pragma Annotate to Control Rule Exemption::
* gnatcheck Annotations Rules::
@end menu

@node Using pragma Annotate to Control Rule Exemption
@section Using pragma @code{Annotate} to Control Rule Exemption
@cindex Using pragma Annotate to control rule exemption

@noindent
Rule exemption is controlled by pragma @code{Annotate} when its first
argument is ``gnatcheck''. The syntax of @command{gnatcheck}'s
exemption control annotations is as follows:

@smallexample @c ada
@group
pragma Annotate (gnatcheck, @i{exemption_control}, @i{Rule_Name}, [@i{justification}]);

@i{exemption_control} ::= Exempt_On | Exempt_Off

@i{Rule_Name}         ::= string_literal

@i{justification}     ::= string_literal
@end group
@end smallexample

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

The @i{@code{Rule_Name}} argument should be the name of some existing
@command{gnatcheck} rule.
Otherwise a warning message is generated and the pragma is
ignored. If @code{Rule_Name} denotes a rule that is not activated by the given
@command{gnatcheck} call, the pragma is ignored and no warning is issued. The
exception from this rule is that exemption sections for @code{Warnings} rule are
fully processed when @code{Restrictions} rule is activated.

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

@smallexample @c ada
pragma Annotate (gnatcheck, Exempt_On, Rule_Name, "justification");
-- source code section
pragma Annotate (gnatcheck, Exempt_Off, Rule_Name);
@end smallexample


@node gnatcheck Annotations Rules
@section @command{gnatcheck} Annotations Rules
@cindex @command{gnatcheck} annotations rules

@itemize @bullet

@item
An ``Exempt_Off'' annotation can only appear after a corresponding
``Exempt_On'' annotation.

@item
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.

@item
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.

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

@item
When an exempted source code section does not contain at least one violation
of the exempted rule, a warning is emitted on @file{stderr}.

@item
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.
@end itemize


@c ***********************
@node Predefined Rules
@c ***********************
@chapter Predefined Rules
@cindex Predefined Rules

The description of the rules currently implemented in @command{gnatcheck} is
given in this chapter.
The rule identifier is
used as a parameter of @command{gnatcheck}'s @option{+R} or @option{-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.

@menu
* Style-Related Rules::
* Feature Usage Rules::
* Metrics-Related Rules::
* SPARK Ada Rules::
@end menu

@c ***********************
@node Style-Related Rules
@c ***********************
@section Style-Related Rules
@cindex Style-related rules

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

@menu
* Tasking::
* Object Orientation::
* Portability::
* Program Structure::
* Programming Practice::
* Readability::
* Source Code Presentation::
@end menu


@c ---------
@node Tasking
@subsection Tasking
@cindex Tasking-related rules

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

@menu
* Multiple_Entries_In_Protected_Definitions::
* Volatile_Objects_Without_Address_Clauses::
@end menu

@node Multiple_Entries_In_Protected_Definitions
@subsubsection @code{Multiple_Entries_In_Protected_Definitions}
@cindex @code{Multiple_Entries_In_Protected_Definitions}

@noindent
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.


@node Volatile_Objects_Without_Address_Clauses
@subsubsection @code{Volatile_Objects_Without_Address_Clauses}
@cindex @code{Volatile_Objects_Without_Address_Clauses}

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

The following check is made: if the pragma @code{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
@code{Volatile_Components}, or objects that are volatile because
they are atomic as a result of pragmas @code{Atomic} or
@code{Atomic_Components}.

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

This rule has no parameters.


@c ---------
@node Object Orientation
@subsection Object Orientation
@cindex Object-Orientation related rules

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

@menu
* Deep_Inheritance_Hierarchies::
* Direct_Calls_To_Primitives::
* Too_Many_Parents::
* Visible_Components::
@end menu

@node Deep_Inheritance_Hierarchies
@subsubsection @code{Deep_Inheritance_Hierarchies}
@cindex @code{Deep_Inheritance_Hierarchies}

@noindent
Flags a tagged derived type declaration or an interface type declaration if
its depth (in its inheritance
hierarchy) exceeds the value specified by the @option{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 @option{+R} option:

@table @emph
@item 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.
@end table


@node Direct_Calls_To_Primitives
@subsubsection @code{Direct_Calls_To_Primitives}
@cindex @code{Direct_Calls_To_Primitives}

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

@itemize @bullet

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

@item
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;

@end itemize

This rule has no parameters.


@node Too_Many_Parents
@subsubsection @code{Too_Many_Parents}
@cindex @code{Too_Many_Parents}

@noindent
Flags any type declaration, single task declaration or single protected
declaration that has more then  @option{N} parents,  @option{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 @option{+R} option:

@table @emph
@item N
Positive integer specifying the maximal allowed number of parents.
@end table


@node Visible_Components
@subsubsection @code{Visible_Components}
@cindex @code{Visible_Components}

@noindent
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.


@c ---------
@node Portability
@subsection Portability
@cindex Portability-related rules

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

@menu
* Forbidden_Attributes::
* Forbidden_Pragmas::
* Implicit_SMALL_For_Fixed_Point_Types::
* Predefined_Numeric_Types::
* Separate_Numeric_Error_Handlers::
@end menu


@node Forbidden_Attributes
@subsubsection @code{Forbidden_Attributes}
@cindex @code{Forbidden_Attributes}

@noindent
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:

@itemize @bullet
@item For the @option{+R} option

@table @asis
@item @emph{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 @emph{Attribute_Designator}
does not denote any attribute defined in the Ada standard
or in
@ref{Implementation Defined Attributes,,, gnat_rm, GNAT Reference
Manual}, it is treated as the name of unknown attribute.

@item @code{GNAT}
All the GNAT-specific attributes are detected; this sets
the detection checks for all the specified attributes ON.

@item @code{ALL}
All attributes are detected; this sets the rule ON.
@end table

@item For the @option{-R} option
@table @asis
@item @emph{Attribute_Designator}
Removes the specified attribute from the set of attributes to be
detected without affecting detection checks for
other attributes. If @emph{Attribute_Designator} does not correspond to any
attribute defined in the Ada standard or in
@ref{Implementation Defined Attributes,,, gnat_rm, GNAT Reference Manual},
this option is treated as turning OFF detection of all unknown attributes.

@item GNAT
Turn OFF detection of all GNAT-specific attributes

@item ALL
Clear the list of the attributes to be detected and
turn the rule OFF.
@end table
@end itemize

@noindent
Parameters are not case sensitive. If @emph{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 @option{+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
@option{+RForbidden_Attributes} (with
no parameter), then the rule is enabled, but it does not detect anything).
The @option{-R} option with no parameter turns the rule OFF, but it does not
affect the set of attributes to be detected.


@node Forbidden_Pragmas
@subsubsection @code{Forbidden_Pragmas}
@cindex @code{Forbidden_Pragmas}

@noindent
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:

@itemize @bullet
@item For the @option{+R} option

@table @asis
@item @emph{Pragma_Name}
Adds the specified pragma to the set of pragmas to be
checked and sets the checks for all the specified pragmas
ON. @emph{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 @ref{Implementation Defined Pragmas,,, gnat_rm, GNAT Reference
Manual}, it is treated as the name of unknown pragma.

@item @code{GNAT}
All the GNAT-specific pragmas are detected; this sets
the checks for all the specified pragmas ON.

@item @code{ALL}
All pragmas are detected; this sets the rule ON.
@end table

@item For the @option{-R} option
@table @asis
@item @emph{Pragma_Name}
Removes the specified pragma from the set of pragmas to be
checked without affecting checks for
other pragmas. @emph{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
@ref{Implementation Defined Pragmas,,, gnat_rm, GNAT Reference Manual},
this option is treated as turning OFF detection of all unknown pragmas.

@item GNAT
Turn OFF detection of all GNAT-specific pragmas

@item ALL
Clear the list of the pragmas to be detected and
turn the rule OFF.
@end table
@end itemize

@noindent
Parameters are not case sensitive. If @emph{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 @command{gnatcheck}
call, a new option overrides the previous one(s).

The @option{+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
@option{+RForbidden_Pragmas} (with
no parameter), then the rule is enabled, but it does not detect anything).
The @option{-R} option with no parameter turns the rule OFF, but it does not
affect the set of pragmas to be detected.



@node Implicit_SMALL_For_Fixed_Point_Types
@subsubsection @code{Implicit_SMALL_For_Fixed_Point_Types}
@cindex @code{Implicit_SMALL_For_Fixed_Point_Types}

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

This rule has no parameters.


@node Predefined_Numeric_Types
@subsubsection @code{Predefined_Numeric_Types}
@cindex @code{Predefined_Numeric_Types}

@noindent
Flag each explicit use of the name of any numeric type or subtype defined
in package @code{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 @code{String} indexing
likely needs a variable of type @code{Integer}.
Another example is the flagging of predefined numeric types with explicit
constraints:

@smallexample @c ada
    subtype My_Integer is Integer range Left .. Right;
    Vy_Var : My_Integer;
@end smallexample

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

This rule has no parameters.


@node Separate_Numeric_Error_Handlers
@subsubsection @code{Separate_Numeric_Error_Handlers}
@cindex @code{Separate_Numeric_Error_Handlers}

@noindent
Flags each exception handler that contains a choice for
the predefined @code{Constraint_Error} exception, but does not contain
the choice for the predefined @code{Numeric_Error} exception, or
that contains the choice for @code{Numeric_Error}, but does not contain the
choice for @code{Constraint_Error}.

This rule has no parameters.


@c ---------
@node Program Structure
@subsection Program Structure
@cindex Program Structure related rules

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

@menu
* Deeply_Nested_Generics::
* Local_Packages::
* Non_Visible_Exceptions::
* Raising_External_Exceptions::
@end menu

@node Deeply_Nested_Generics
@subsubsection @code{Deeply_Nested_Generics}
@cindex @code{Deeply_Nested_Generics}

@noindent
Flags a generic declaration nested in another generic declaration if
the nesting level of the inner generic exceeds
a value specified by the @option{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 @option{+R} option:

@table @emph
@item N
Positive integer specifying the maximal allowed nesting level
for a generic declaration.
@end table


@node Local_Packages
@subsubsection @code{Local_Packages}
@cindex @code{Local_Packages}

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

This rule has no parameters.


@node Non_Visible_Exceptions
@subsubsection @code{Non_Visible_Exceptions}
@cindex @code{Non_Visible_Exceptions} rule

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

@itemize @bullet
@item
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 @code{others} choice.

@item
A @code{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:
@itemize @minus
@item
it explicitly raises a locally declared exception, or
@item
it does not specify an exception name (i.e., it is simply @code{raise;})
and the enclosing handler contains a locally declared exception in its
exception choices.
@end itemize
@end itemize

@noindent
Renamings of local exceptions are not flagged.

This rule has no parameters.


@node Raising_External_Exceptions
@subsubsection @code{Raising_External_Exceptions}
@cindex @code{Raising_External_Exceptions}

@noindent
Flag any @code{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.




@c ---------
@node Programming Practice
@subsection Programming Practice
@cindex Programming Practice related rules

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

@menu
* Anonymous_Arrays::
* Enumeration_Ranges_In_CASE_Statements::
* Exceptions_As_Control_Flow::
* Exits_From_Conditional_Loops::
* EXIT_Statements_With_No_Loop_Name::
* GOTO_Statements::
* Improper_Returns::
* Non_Short_Circuit_Operators::
* OTHERS_In_Aggregates::
* OTHERS_In_CASE_Statements::
* OTHERS_In_Exception_Handlers::
* Overly_Nested_Control_Structures::
* Positional_Actuals_For_Defaulted_Generic_Parameters::
* Positional_Actuals_For_Defaulted_Parameters::
* Positional_Components::
* Positional_Generic_Parameters::
* Positional_Parameters::
* Recursive_Subprograms::
* Unconditional_Exits::
* Unnamed_Blocks_And_Loops::
* USE_PACKAGE_Clauses::
@end menu

@node Anonymous_Arrays
@subsubsection @code{Anonymous_Arrays}
@cindex @code{Anonymous_Arrays}

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

This rule has no parameters.


@node Enumeration_Ranges_In_CASE_Statements
@subsubsection @code{Enumeration_Ranges_In_CASE_Statements}
@cindex @code{Enumeration_Ranges_In_CASE_Statements}

@noindent
Flag each use of a range of enumeration literals as a choice in a
@code{case} statement.
All forms for specifying a range (explicit ranges
such as @code{A .. B}, subtype marks and @code{'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
@code{case} statement with an enumeration range that includes the new literal.

This rule has no parameters.


@node Exceptions_As_Control_Flow
@subsubsection @code{Exceptions_As_Control_Flow}
@cindex @code{Exceptions_As_Control_Flow}

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

The rule has no parameters.


@node Exits_From_Conditional_Loops
@subsubsection @code{Exits_From_Conditional_Loops}
@cindex @code{Exits_From_Conditional_Loops}

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

The rule has no parameters.


@node EXIT_Statements_With_No_Loop_Name
@subsubsection @code{EXIT_Statements_With_No_Loop_Name}
@cindex @code{EXIT_Statements_With_No_Loop_Name}

@noindent
Flag each @code{exit} statement that does not specify the name of the loop
being exited.

The rule has no parameters.


@node GOTO_Statements
@subsubsection @code{GOTO_Statements}
@cindex @code{GOTO_Statements}

@noindent
Flag each occurrence of a @code{goto} statement.

This rule has no parameters.


@node Improper_Returns
@subsubsection @code{Improper_Returns}
@cindex @code{Improper_Returns}

@noindent
Flag each explicit @code{return} statement in procedures, and
multiple @code{return} statements in functions.
Diagnostic messages are generated for all @code{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 @code{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.


@node Non_Short_Circuit_Operators
@subsubsection @code{Non_Short_Circuit_Operators}
@cindex @code{Non_Short_Circuit_Operators}

@noindent
Flag all calls to predefined @code{and} and @code{or} operators for
any boolean type. Calls to
user-defined @code{and} and @code{or} and to operators defined by renaming
declarations are not flagged. Calls to predefined @code{and} and @code{or}
operators for modular types or boolean array types are not flagged.

This rule has no parameters.


@node OTHERS_In_Aggregates
@subsubsection @code{OTHERS_In_Aggregates}
@cindex @code{OTHERS_In_Aggregates}

@noindent
Flag each use of an @code{others} choice in extension aggregates.
In record and array aggregates, an @code{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 @code{others} choice and another with a discrete range, the
@code{others} choice is flagged even if the discrete range specifies
exactly one component; for example, @code{(1..1 => 0, others => 1)}.

This rule has no parameters.


@node OTHERS_In_CASE_Statements
@subsubsection @code{OTHERS_In_CASE_Statements}
@cindex @code{OTHERS_In_CASE_Statements}

@noindent
Flag any use of an @code{others} choice in a @code{case} statement.

This rule has no parameters.


@node OTHERS_In_Exception_Handlers
@subsubsection @code{OTHERS_In_Exception_Handlers}
@cindex @code{OTHERS_In_Exception_Handlers}

@noindent
Flag any use of an @code{others} choice in an exception handler.

This rule has no parameters.


@node Overly_Nested_Control_Structures
@subsubsection @code{Overly_Nested_Control_Structures}
@cindex @code{Overly_Nested_Control_Structures}

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

The control structures checked are the following:

@itemize @bullet
@item    @code{if} statement
@item    @code{case} statement
@item    @code{loop} statement
@item    Selective accept statement
@item    Timed entry call statement
@item    Conditional entry call
@item    Asynchronous select statement
@end itemize

@noindent
The rule has the following parameter for the @option{+R} option:

@table @emph
@item N
Positive integer specifying the maximal control structure nesting
level that is not flagged
@end table

@noindent
If the parameter for the @option{+R} option is not specified or
if it is not a positive integer, @option{+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).


@node Positional_Actuals_For_Defaulted_Generic_Parameters
@subsubsection @code{Positional_Actuals_For_Defaulted_Generic_Parameters}
@cindex @code{Positional_Actuals_For_Defaulted_Generic_Parameters}

@noindent
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.


@node Positional_Actuals_For_Defaulted_Parameters
@subsubsection @code{Positional_Actuals_For_Defaulted_Parameters}
@cindex @code{Positional_Actuals_For_Defaulted_Parameters} rule

@noindent
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.


@node Positional_Components
@subsubsection @code{Positional_Components}
@cindex @code{Positional_Components}

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

This rule has no parameters.


@node Positional_Generic_Parameters
@subsubsection @code{Positional_Generic_Parameters}
@cindex @code{Positional_Generic_Parameters}

@noindent
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.


@node Positional_Parameters
@subsubsection @code{Positional_Parameters}
@cindex @code{Positional_Parameters}

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

@itemize @bullet
@item
Parameters of calls to of prefix or infix operators are not flagged
@item
If the called subprogram or entry has only one formal parameter,
the parameter of the call is not flagged;
@item
If a subprogram call uses the @emph{Object.Operation} notation, then
@itemize @minus
@item
the first parameter (that is, @emph{Object}) is not flagged;
@item
if the called subprogram has only two parameters, the second parameter
of the call is not flagged;
@end itemize
@end itemize

@noindent
This rule has no parameters.


@node Recursive_Subprograms
@subsubsection @code{Recursive_Subprograms}
@cindex @code{Recursive_Subprograms} rule

@noindent

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.


@node Unconditional_Exits
@subsubsection @code{Unconditional_Exits}
@cindex @code{Unconditional_Exits} rule

@noindent
Flag unconditional @code{exit} statements.

This rule has no parameters.


@node Unnamed_Blocks_And_Loops
@subsubsection @code{Unnamed_Blocks_And_Loops}
@cindex @code{Unnamed_Blocks_And_Loops}

@noindent
Flag each unnamed block statement and loop statement.

The rule has no parameters.


@node USE_PACKAGE_Clauses
@subsubsection @code{USE_PACKAGE_Clauses}
@cindex @code{USE_PACKAGE_Clauses}

@noindent
Flag all @code{use} clauses for packages; @code{use type} clauses are
not flagged.

This rule has no parameters.



@c ---------
@node Readability
@subsection Readability
@cindex Readability-related rules

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

@menu
* Misnamed_Controlling_Parameters::
* Misnamed_Identifiers::
* Name_Clashes::
* Uncommented_BEGIN_In_Package_Bodies::
@end menu

@node Misnamed_Controlling_Parameters
@subsubsection @code{Misnamed_Controlling_Parameters}
@cindex @code{Misnamed_Controlling_Parameters}

@noindent
Flags a declaration of a dispatching operation, if the first parameter is
not a controlling one and its name is not @code{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.


@node Misnamed_Identifiers
@subsubsection @code{Misnamed_Identifiers}
@cindex @code{Misnamed_Identifiers}

@noindent
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:

@itemize @bullet
@item
type declarations

@item
subtype declarations

@item
constant declarations (but not number declarations)

@item
package renaming declarations (but not generic package renaming
declarations)
@end itemize

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

@itemize @bullet
@item
type-defining names end with @code{_T}, unless the type is an access type,
in which case the suffix must be @code{_A}
@item
constant names end with @code{_C}
@item
names defining package renamings end with @code{_R}
@end itemize

@noindent
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.

@noindent
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:

@itemize @bullet
@item
For the @option{+R} option:
@table @code
@item Default
Sets the default listed above for all the names to be checked.

@item Type_Suffix=@emph{string}
Specifies the suffix for a type name.

@item Access_Suffix=@emph{string}
Specifies the suffix for an access type name. If
this parameter is set, it overrides for access
types the suffix set by the @code{Type_Suffix} parameter.
For access types, @emph{string} may have the following format:
@emph{suffix1(suffix2)}. That means that an access type name
should have the @emph{suffix1} suffix except for the case when
the designated type is also an access type, in this case the
type name should have the @emph{suffix1 & suffix2} suffix.

@item Class_Access_Suffix=@emph{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 @code{Type_Suffix} or @code{Access_Suffix}
parameter.

@item Class_Subtype_Suffix=@emph{string}
Specifies the suffix for the name of a subtype that denotes a class-wide type.

@item Constant_Suffix=@emph{string}
Specifies the suffix for a constant name.

@item Renaming_Suffix=@emph{string}
Specifies the suffix for a package renaming name.
@end table

@item
For the @option{-R} option:
@table @code
@item 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.

@item 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 @code{Access_Suffix} is
set).

@item 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 @code{Type_Suffix} is set, access type names are
checked as ordinary type names.

@item 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 @code{Type_Suffix} is set, access type names are
checked as ordinary type names. If @code{Access_Suffix} is set, these
access types are checked as any other access type name.

@item Class_Subtype_Suffix=@emph{string}
Removes the suffix specified for subtype names.
This disables checks for subtype names but
does not disable any other checks for this rule.

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

@item 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.
@end table
@end itemize

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

If more than one  option is specified for the @command{gnatcheck} invocation,
a new option overrides the previous one(s).

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

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

The @emph{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 @emph{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.


@node Name_Clashes
@subsubsection @code{Name_Clashes}
@cindex @code{Name_Clashes}

@noindent
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 @code{--} to end-of-line).
Identifiers must follow the Ada syntax for identifiers.
A line containing one or more identifiers may end with a comment.


@node Uncommented_BEGIN_In_Package_Bodies
@subsubsection @code{Uncommented_BEGIN_In_Package_Bodies}
@cindex @code{Uncommented_BEGIN_In_Package_Bodies}

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

If the @code{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.



@c ---------
@node Source Code Presentation
@subsection Source Code Presentation
@cindex Source code presentation related rules

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

@c **********************
@node Feature Usage Rules
@c **********************
@section Feature Usage Rules
@cindex Feature usage related rules

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

@menu
* Abstract_Type_Declarations::
* Anonymous_Subtypes::
* Blocks::
* Complex_Inlined_Subprograms::
* Controlled_Type_Declarations::
* Declarations_In_Blocks::
* Deeply_Nested_Inlining::
* Default_Parameters::
* Discriminated_Records::
* Explicit_Full_Discrete_Ranges::
* Float_Equality_Checks::
* Function_Style_Procedures::
* Generics_In_Subprograms::
* Implicit_IN_Mode_Parameters::
* Improperly_Located_Instantiations::
* Library_Level_Subprograms::
* Non_Qualified_Aggregates::
* Numeric_Literals::
* Parameters_Out_Of_Order::
* Raising_Predefined_Exceptions::
* Unassigned_OUT_Parameters::
* Unconstrained_Array_Returns::
@end menu

@node Abstract_Type_Declarations
@subsection @code{Abstract_Type_Declarations}
@cindex @code{Abstract_Type_Declarations}

@noindent
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.

@node Anonymous_Subtypes
@subsection @code{Anonymous_Subtypes}
@cindex @code{Anonymous_Subtypes}

@noindent
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 @code{for} loops such as the following are
flagged (since @code{1..N} is formally a ``range''):

@smallexample @c ada
for I in 1 .. N loop
   @dots{}
end loop;
@end smallexample

@noindent
Declaring an explicit subtype solves the problem:

@smallexample @c ada
subtype S is Integer range 1..N;
@dots{}
for I in S loop
   @dots{}
end loop;
@end smallexample

@noindent
This rule has no parameters.

@node Blocks
@subsection @code{Blocks}
@cindex @code{Blocks}

@noindent
Flag each block statement.

This rule has no parameters.


@node Complex_Inlined_Subprograms
@subsection @code{Complex_Inlined_Subprograms}
@cindex @code{Complex_Inlined_Subprograms}

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

@itemize @bullet
@item
it contains at least one complex declaration such as a subprogram body,
package, task, protected declaration, or a generic instantiation
(except instantiation of @code{Ada.Unchecked_Conversion});

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

@item
the number of statements exceeds
a value specified by the @option{N} rule parameter;
@end itemize

@noindent
This rule has the following (mandatory) parameter for the @option{+R} option:

@table @emph
@item N
Positive integer specifying the maximum allowed total number of statements
in the subprogram body.
@end table


@node Controlled_Type_Declarations
@subsection @code{Controlled_Type_Declarations}
@cindex @code{Controlled_Type_Declarations}

@noindent
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 @code{Ada.Finalization} but has a controlled
component is not checked.

This rule has no parameters.


@node Declarations_In_Blocks
@subsection @code{Declarations_In_Blocks}
@cindex @code{Declarations_In_Blocks}

@noindent
Flag all block statements containing local declarations. A @code{declare}
block with an empty @i{declarative_part} or with a @i{declarative part}
containing only pragmas and/or @code{use} clauses is not flagged.

This rule has no parameters.


@node Deeply_Nested_Inlining
@subsection @code{Deeply_Nested_Inlining}
@cindex @code{Deeply_Nested_Inlining}

@noindent
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
@option{N} rule parameter.

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

This rule has the following (mandatory) parameter for the @option{+R} option:

@table @emph
@item N
Positive integer specifying the maximal allowed level of nested inlining.
@end table


@node Default_Parameters
@subsection @code{Default_Parameters}
@cindex @code{Default_Parameters}

@noindent
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.


@node Discriminated_Records
@subsection @code{Discriminated_Records}
@cindex @code{Discriminated_Records}

@noindent
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.


@node Explicit_Full_Discrete_Ranges
@subsection @code{Explicit_Full_Discrete_Ranges}
@cindex @code{Explicit_Full_Discrete_Ranges}

@noindent
Flag each discrete range that has the form @code{A'First .. A'Last}.

This rule has no parameters.


@node Float_Equality_Checks
@subsection @code{Float_Equality_Checks}
@cindex @code{Float_Equality_Checks}

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

This rule has no parameters.


@node Function_Style_Procedures
@subsection @code{Function_Style_Procedures}
@cindex @code{Function_Style_Procedures}

@noindent
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 @code{out}
and no parameters of mode @code{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 @code{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.


@node Generics_In_Subprograms
@subsection @code{Generics_In_Subprograms}
@cindex @code{Generics_In_Subprograms}

@noindent
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.


@node Implicit_IN_Mode_Parameters
@subsection @code{Implicit_IN_Mode_Parameters}
@cindex @code{Implicit_IN_Mode_Parameters}

@noindent
Flag each occurrence of a formal parameter with an implicit @code{in} mode.
Note that @code{access} parameters, although they technically behave
like @code{in} parameters, are not flagged.

This rule has no parameters.


@node Improperly_Located_Instantiations
@subsection @code{Improperly_Located_Instantiations}
@cindex @code{Improperly_Located_Instantiations}

@noindent
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.


@node Library_Level_Subprograms
@subsection @code{Library_Level_Subprograms}
@cindex @code{Library_Level_Subprograms}

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

This rule has no parameters.

@node Non_Qualified_Aggregates
@subsection @code{Non_Qualified_Aggregates}
@cindex @code{Non_Qualified_Aggregates}

@noindent
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.


@node Numeric_Literals
@subsection @code{Numeric_Literals}
@cindex @code{Numeric_Literals}

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

@itemize @bullet
@item
a literal occurring in the initialization expression for a constant
declaration or a named number declaration, or

@item
an integer literal that is less than or equal to a value
specified by the @option{N} rule parameter.

@item
a literal occurring in a declaration in case the @option{Statements_Only}
rule parameter is given
@end itemize

@noindent
This rule may have the following parameters for the @option{+R} option:

@table @asis
@item @emph{N}
@emph{N} is an integer literal used as the maximal value that is not flagged
(i.e., integer literals not exceeding this value are allowed)

@item @code{ALL}
All integer literals are flagged

@item @code{Statements_Only}
Numeric literals are flagged only when used in statements
@end table

@noindent
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 @option{+R} options appear.

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


@node Parameters_Out_Of_Order
@subsection @code{Parameters_Out_Of_Order}
@cindex @code{Parameters_Out_Of_Order}

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

@itemize @bullet

@item @code{in} and @code{access} parameters first,
then @code{in out} parameters,
and then @code{out} parameters;

@item for @code{in} mode, parameters with default initialization expressions
occur last
@end itemize

@noindent
Only the first violation of the described order is flagged.

The following constructs are checked:

@itemize @bullet
@item   subprogram declarations (including null procedures);
@item   generic subprogram declarations;
@item   formal subprogram declarations;
@item   entry declarations;
@item   subprogram bodies and subprogram body stubs that do not
have separate specifications
@end itemize

@noindent
Subprogram renamings are not checked.

This rule has no parameters.


@node Raising_Predefined_Exceptions
@subsection @code{Raising_Predefined_Exceptions}
@cindex @code{Raising_Predefined_Exceptions}

@noindent
Flag each @code{raise} statement that raises a predefined exception
(i.e., one of the exceptions @code{Constraint_Error}, @code{Numeric_Error},
@code{Program_Error}, @code{Storage_Error}, or @code{Tasking_Error}).

This rule has no parameters.


@node Unassigned_OUT_Parameters
@subsection @code{Unassigned_OUT_Parameters}
@cindex @code{Unassigned_OUT_Parameters}

@noindent
Flags procedures' @code{out} parameters that are not assigned, and
identifies the contexts in which the assignments are missing.

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

An @code{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 @code{raise} statement.

Bodies of generic procedures are also considered.

The following are treated as assignments to an @code{out} parameter:

@itemize @bullet
@item
an assignment statement, with the parameter or some component as the target;

@item
passing the parameter (or one of its components) as an @code{out} or
@code{in out} parameter.
@end itemize

@noindent
This rule does not have any parameters.


@node Unconstrained_Array_Returns
@subsection @code{Unconstrained_Array_Returns}
@cindex @code{Unconstrained_Array_Returns}

@noindent
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 @option{+R} option:

@table @emph
@item Except_String
Do not flag functions that return the predefined @code{String} type or a type
derived from it, directly or indirectly.
@end table


@c **************************
@node Metrics-Related Rules
@c **************************
@section Metrics-Related Rules
@cindex Metrics-related rules

@noindent
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.

@menu
* Metrics_Essential_Complexity::
* Metrics_Cyclomatic_Complexity::
* Metrics_LSLOC::
@end menu

The name of any metrics rule consists of the prefix @code{Metrics_}
followed by the name of the corresponding metric:
@code{Essential_Complexity}, @code{Cyclomatic_Complexity}, or
@code{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 @command{gnatmetric}.

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

@noindent
@emph{Example:} the rule
@smallexample
+RMetrics_Cyclomatic_Complexity : 7
@end smallexample
@noindent
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:
@smallexample
-RMetrics_Cyclomatic_Complexity
@end smallexample

@ignore
@c This is from the earlier version
@multitable {@code{Cyclomatic_Complexity}}{Cyclomatic complexity}{Positive integer}
@ifnothtml
@headitem Check Name @tab Description @tab Bounds Value
@end ifnothtml
@ifhtml
@item @b{Check Name} @tab @b{Description} @tab @b{Bounds Value}
@end ifhtml
@c Above conditional code is workaround to bug in texi2html (Feb 2008)
@item @code{Essential_Complexity} @tab Essential complexity @tab Positive integer (U)
@item @code{Cyclomatic_Complexity} @tab Cyclomatic complexity @tab Positive integer (U)
@item @code{LSLOC} @tab Logical Source Lines of Code @tab Positive integer (U)
@end multitable
@end ignore


@node Metrics_Essential_Complexity
@subsection @code{Metrics_Essential_Complexity}
@cindex @code{Metrics_Essential_Complexity}

@noindent
The @code{Metrics_Essential_Complexity} rule takes a positive integer as
upper bound.  A construct exceeding this limit will be flagged.


@node Metrics_Cyclomatic_Complexity
@subsection @code{Metrics_Cyclomatic_Complexity}
@cindex @code{Metrics_Cyclomatic_Complexity}

@noindent
The @code{Metrics_Cyclomatic_Complexity} rule takes a positive integer as
upper bound.  A construct exceeding this limit will be flagged.


@node Metrics_LSLOC
@subsection @code{Metrics_LSLOC}
@cindex @code{Metrics_LSLOC}

@noindent
The @code{Metrics_LSLOC} rule takes a positive integer as
upper bound.  A compilation unit exceeding this limit will be flagged.




@c *******************
@node SPARK Ada  Rules
@c *******************
@section SPARK Ada Rules
@cindex SPARK Ada related rules

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

@menu
* Annotated_Comments::
* Boolean_Relational_Operators::
* Expanded_Loop_Exit_Names::
* Non_SPARK_Attributes::
* Non_Tagged_Derived_Types::
* Outer_Loop_Exits::
* Overloaded_Operators::
* Slices::
* Universal_Ranges::
@end menu

@node Annotated_Comments
@subsection @code{Annotated_Comments}
@cindex @code{Annotated_Comments}

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

@smallexample
  --<special_character> <comment_marker>
@end smallexample

@noindent
where

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

@item <comment_marker>
a word identifying the annotation or special usage (word here is any sequence
of characters except white space)
@end table

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

@code{<comment_marker>} must not contain any white space.

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

The rule has the following (mandatory) parameter for the @option{+R} option:

@table @emph
@item 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.
@end table

@noindent
The @option{-R} option erases all definitions of special comment annotations
specified by the previous +R options.

The rule is case-sensitive.

Example:

The rule

+R@smallexample
Annotated_Comments:#hide
@end smallexample

@noindent
will flag the following comment lines

+R@smallexample
--#hide
--# hide
--#           hide

   I := I + 1; --# hide
@end smallexample

@noindent
But the line

+R@smallexample
-- # hide
@end smallexample

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

The line

+R@smallexample
--#Hide
@end smallexample

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

@node Boolean_Relational_Operators
@subsection @code{Boolean_Relational_Operators}
@cindex @code{Boolean_Relational_Operators}

@noindent
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
@code{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 @code{Standard.Boolean},
are likewise not detected.

This rule has no parameters.


@node Expanded_Loop_Exit_Names
@subsection @code{Expanded_Loop_Exit_Names}
@cindex @code{Expanded_Loop_Exit_Names}

@noindent
Flag all expanded loop names in @code{exit} statements.

This rule has no parameters.

@node Non_SPARK_Attributes
@subsection @code{Non_SPARK_Attributes}
@cindex @code{Non_SPARK_Attributes}

@noindent
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.

@itemize @bullet
@item @code{'Adjacent}
@item @code{'Aft}
@item @code{'Base}
@item @code{'Ceiling}
@item @code{'Component_Size}
@item @code{'Compose}
@item @code{'Copy_Sign}
@item @code{'Delta}
@item @code{'Denorm}
@item @code{'Digits}
@item @code{'Exponent}
@item @code{'First}
@item @code{'Floor}
@item @code{'Fore}
@item @code{'Fraction}
@item @code{'Last}
@item @code{'Leading_Part}
@item @code{'Length}
@item @code{'Machine}
@item @code{'Machine_Emax}
@item @code{'Machine_Emin}
@item @code{'Machine_Mantissa}
@item @code{'Machine_Overflows}
@item @code{'Machine_Radix}
@item @code{'Machine_Rounds}
@item @code{'Max}
@item @code{'Min}
@item @code{'Model}
@item @code{'Model_Emin}
@item @code{'Model_Epsilon}
@item @code{'Model_Mantissa}
@item @code{'Model_Small}
@item @code{'Modulus}
@item @code{'Pos}
@item @code{'Pred}
@item @code{'Range}
@item @code{'Remainder}
@item @code{'Rounding}
@item @code{'Safe_First}
@item @code{'Safe_Last}
@item @code{'Scaling}
@item @code{'Signed_Zeros}
@item @code{'Size}
@item @code{'Small}
@item @code{'Succ}
@item @code{'Truncation}
@item @code{'Unbiased_Rounding}
@item @code{'Val}
@item @code{'Valid}
@end itemize

@noindent
This rule has no parameters.


@node Non_Tagged_Derived_Types
@subsection @code{Non_Tagged_Derived_Types}
@cindex @code{Non_Tagged_Derived_Types}

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

This rule has no parameters.


@node Outer_Loop_Exits
@subsection @code{Outer_Loop_Exits}
@cindex @code{Outer_Loop_Exits}

@noindent
Flag each @code{exit} statement containing a loop name that is not the name
of the immediately enclosing @code{loop} statement.

This rule has no parameters.


@node Overloaded_Operators
@subsection @code{Overloaded_Operators}
@cindex @code{Overloaded_Operators}

@noindent
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.


@node Slices
@subsection @code{Slices}
@cindex @code{Slices}

@noindent
Flag all uses of array slicing

This rule has no parameters.


@node Universal_Ranges
@subsection @code{Universal_Ranges}
@cindex @code{Universal_Ranges} rule

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

This rule has no parameters.



@c *******************************************
@c Text for rules that are not yet implemented
@c *******************************************

@c -------
@ignore
@node Ceiling_Violations
@section @code{Ceiling5_Violations} (under construction, GLOBAL)
@cindex @code{Ceiling_Violations} rule

@noindent
Flag invocations of a protected operation by a task whose priority exceeds
the protected object's ceiling.

As of @value{NOW}, this rule has the following limitations:

@itemize @bullet

@item
 We consider only pragmas Priority and Interrupt_Priority as means to define
  a task/protected operation priority. We do not consider the effect of using
  Ada.Dynamic_Priorities.Set_Priority procedure;

@item
 We consider only base task priorities, and no priority inheritance. That is,
  we do not make a difference between calls issued during task activation and
  execution of the sequence of statements from task body;

@item
 Any situation when the priority of protected operation caller is set by a
  dynamic expression (that is, the corresponding Priority or
  Interrupt_Priority pragma has a non-static expression as an argument) we
  treat as a priority inconsistency (and, therefore, detect this situation).
@end itemize

@noindent
At the moment the notion of the main subprogram is not implemented in
gnatcheck, so any pragma Priority in a library level subprogram body (in case
if this subprogram can be a main subprogram of a partition) changes the
priority of an environment task. So if we have more then one such pragma in
the set of processed sources, the pragma that is processed last, defines the
priority of an environment task.

This rule has no parameters.
@end ignore
@c -------

@c -------
@ignore
@node Deeply_Nested_Local_Inlining
@section @code{Deeply_Nested_Local_Inlining}
@cindex @code{Deeply_Nested_Local_Inlining} rule

@noindent
Flags a subprogram body if a pragma @code{Inline} is applied to the
corresponding subprogram (or generic subprogram) and the body contains a call
to another inlined subprogram that results in nested inlining with nesting
depth more then a value specified by the @option{N} rule parameter.
This rule is similar to @code{Deeply_Nested_Inlining} rule, but it
assumes that calls to subprograms in
with'ed units are not inlined, so all the analysis of the depth of inlining is
limited by the compilation unit where the subprogram body is located and the
units it depends semantically upon. Such analysis may be useful for the case
when neither @option{-gnatn} nor @option{-gnatN} option is used when building
the executable.

This rule has the following (mandatory) parameters for the @option{+R} option:

@table @emph
@item N
Positive integer specifying the maximal allowed level of nested inlining.
@end table

@end ignore
@c -------

@c -------
@ignore
@node Improperly_Called_Protected_Entries
@section @code{Improperly_Called_Protected_Entries} (under construction, GLOBAL)
@cindex @code{Improperly_Called_Protected_Entries} rule

@noindent
Flag each protected entry that can be called from more than one task.

This rule has no parameters.
@end ignore
@c -------

@c -------
@ignore
@node Recursion
@section @code{Recursion} (under construction, GLOBAL)
@cindex @code{Recursion} rule

@noindent
Flag recursive subprograms (cycles in the call graph). Declarations, and not
calls, of recursive subprograms are detected.

This rule has no parameters.
@end ignore
@c -------

@c -------
@ignore
@node Side_Effect_Functions
@section @code{Side_Effect_Functions} (under construction, GLOBAL)
@cindex @code{Side_Effect_Functions} rule

@noindent
Flag functions with side effects.

We define a side effect as changing any data object that is not local for the
body of this function.

At the moment, we do NOT consider a side effect any input-output operations
(changing a state or a content of any file).

We do not consider protected functions for this rule (???)

There are the following sources of side effect:

@enumerate
@item Explicit (or direct) side-effect:

@itemize @bullet
@item
direct assignment to a non-local variable;

@item
direct call to an entity that is known to change some data object that is
     not local for the body of this function (Note, that if F1 calls F2 and F2
     does have a side effect, this does not automatically mean that F1 also
     have a side effect, because it may be the case that F2 is declared in
     F1's body and it changes some data object that is global for F2, but
     local for F1);
@end itemize

@item Indirect side-effect:
@itemize @bullet
@item
Subprogram calls implicitly issued by:
@itemize @bullet
@item
computing initialization expressions from type declarations as a part
         of object elaboration or allocator evaluation;
@item
computing implicit parameters of subprogram or entry calls or generic
         instantiations;
@end itemize

@item
activation of a task that change some non-local data object (directly or
     indirectly);

@item
elaboration code of a package that is a result of a package instantiation;

@item
controlled objects;
@end itemize

@item Situations when we can suspect a side-effect, but the full static check
is either impossible or too hard:
@itemize @bullet
@item
assignment to access variables or to the objects pointed by access
     variables;

@item
call to a subprogram pointed by access-to-subprogram value

@item
dispatching calls;
@end itemize
@end enumerate

@noindent
This rule has no parameters.
@end ignore
@c -------

@c -------
@ignore
@node Unused_Subprograms
@section @code{Unused_Subprograms} (under construction, GLOBAL)
@cindex @code{Unused_Subprograms} rule

@noindent
Flag all unused subprograms.

This rule has no parameters.
@end ignore
@c -------

@c *****************
@node Example of gnatcheck Usage
@c *****************
@chapter Example of @command{gnatcheck} Usage

@noindent
Here is a simple example. Suppose that in the current directory we have a
project file named @file{gnatcheck_example.gpr} with the following content:

@smallexample @c projectfile
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;
@end smallexample

@noindent
And the file named @file{coding_standard} is also located in the current
directory and has the following content:

@smallexample
-----------------------------------------------------
-- 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
@end smallexample

@noindent
And the subdirectory @file{src} contains the following Ada sources:

@file{pack.ads}:

@smallexample @c ada
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;
@end smallexample

@noindent
@file{pack.adb}:

@smallexample @c ada
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;
@end smallexample

@noindent
and @file{main.adb}

@smallexample @c ada
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;
@end smallexample

@noindent
And suppose we call @command{gnatcheck} from the current directory using
the @command{gnat} driver:

@smallexample
   gnat check -Pgnatcheck_example.gpr
@end smallexample

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

@smallexample
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
@end smallexample


@c *****************
@c * List of Rules *
@c *****************
@node List of Rules
@appendix List of Rules

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

@itemize
@item @code{Abstract_Type_Declarations}@*
@xref{Abstract_Type_Declarations}.

@ignore
@item @code{Annotated_Comments}@*
@xref{Annotated_Comments}.
@end ignore

@item @code{Anonymous_Arrays}@*
@xref{Anonymous_Arrays}.

@item @code{Anonymous_Subtypes}@*
@xref{Anonymous_Subtypes}.

@item @code{Blocks}@*
@xref{Blocks}.

@item @code{Boolean_Relational_Operators}@*
@xref{Boolean_Relational_Operators}.

@ignore
@item @code{Ceiling_Violations}
@end ignore

@item @code{Complex_Inlined_Subprograms}@*
@xref{Complex_Inlined_Subprograms}.

@item @code{Controlled_Type_Declarations}@*
@xref{Controlled_Type_Declarations}.

@item @code{Declarations_In_Blocks}@*
@xref{Declarations_In_Blocks}.

@item @code{Deep_Inheritance_Hierarchies}@*
@xref{Deep_Inheritance_Hierarchies}.

@item @code{Deeply_Nested_Generics}@*
@xref{Deeply_Nested_Generics}.

@item @code{Deeply_Nested_Inlining}@*
@xref{Deeply_Nested_Inlining}.

@ignore
@item @code{Deeply_Nested_Local_Inlining}
@end ignore

@item @code{Default_Parameters}@*
@xref{Default_Parameters}.

@item @code{Direct_Calls_To_Primitives}@*
@xref{Direct_Calls_To_Primitives}.

@item @code{Discriminated_Records}@*
@xref{Discriminated_Records}.

@item @code{Enumeration_Ranges_In_CASE_Statements}@*
@xref{Enumeration_Ranges_In_CASE_Statements}.

@item @code{Exceptions_As_Control_Flow}@*
@xref{Exceptions_As_Control_Flow}.

@item @code{Exits_From_Conditional_Loops}@*
@xref{Exits_From_Conditional_Loops}.

@item @code{EXIT_Statements_With_No_Loop_Name}@*
@xref{EXIT_Statements_With_No_Loop_Name}.

@item @code{Expanded_Loop_Exit_Names}@*
@xref{Expanded_Loop_Exit_Names}.

@item @code{Explicit_Full_Discrete_Ranges}@*
@xref{Explicit_Full_Discrete_Ranges}.

@item @code{Float_Equality_Checks}@*
@xref{Float_Equality_Checks}.

@item @code{Forbidden_Attributes}@*
@xref{Forbidden_Attributes}.

@item @code{Forbidden_Pragmas}@*
@xref{Forbidden_Pragmas}.

@item @code{Function_Style_Procedures}@*
@xref{Function_Style_Procedures}.

@item @code{Generics_In_Subprograms}@*
@xref{Generics_In_Subprograms}.

@item @code{GOTO_Statements}@*
@xref{GOTO_Statements}.

@item @code{Implicit_IN_Mode_Parameters}@*
@xref{Implicit_IN_Mode_Parameters}.

@item @code{Implicit_SMALL_For_Fixed_Point_Types}@*
@xref{Implicit_SMALL_For_Fixed_Point_Types}.

@item @code{Improperly_Located_Instantiations}@*
@xref{Improperly_Located_Instantiations}.

@item @code{Improper_Returns}@*
@xref{Improper_Returns}.

@item @code{Library_Level_Subprograms}@*
@xref{Library_Level_Subprograms}.

@item @code{Local_Packages}@*
@xref{Local_Packages}.

@ignore
@item @code{Improperly_Called_Protected_Entries}
@end ignore

@item @code{Metrics_Cyclomatic_Complexity}@*
@xref{Metrics_Cyclomatic_Complexity}.

@item @code{Metrics_Essential_Complexity}@*
@xref{Metrics_Essential_Complexity}.

@item @code{Metrics_LSLOC}@*
@xref{Metrics_LSLOC}.

@item @code{Misnamed_Controlling_Parameters}@*
@xref{Misnamed_Controlling_Parameters}.

@item @code{Misnamed_Identifiers}@*
@xref{Misnamed_Identifiers}.

@item @code{Multiple_Entries_In_Protected_Definitions}@*
@xref{Multiple_Entries_In_Protected_Definitions}.

@item @code{Name_Clashes}@*
@xref{Name_Clashes}.

@item @code{Non_Qualified_Aggregates}@*
@xref{Non_Qualified_Aggregates}.

@item @code{Non_Short_Circuit_Operators}@*
@xref{Non_Short_Circuit_Operators}.

@item @code{Non_SPARK_Attributes}@*
@xref{Non_SPARK_Attributes}.

@item @code{Non_Tagged_Derived_Types}@*
@xref{Non_Tagged_Derived_Types}.

@item @code{Non_Visible_Exceptions}@*
@xref{Non_Visible_Exceptions}.

@item @code{Numeric_Literals}@*
@xref{Numeric_Literals}.

@item @code{OTHERS_In_Aggregates}@*
@xref{OTHERS_In_Aggregates}.

@item @code{OTHERS_In_CASE_Statements}@*
@xref{OTHERS_In_CASE_Statements}.

@item @code{OTHERS_In_Exception_Handlers}@*
@xref{OTHERS_In_Exception_Handlers}.

@item @code{Outer_Loop_Exits}@*
@xref{Outer_Loop_Exits}.

@item @code{Overloaded_Operators}@*
@xref{Overloaded_Operators}.

@item @code{Overly_Nested_Control_Structures}@*
@xref{Overly_Nested_Control_Structures}.

@item @code{Parameters_Out_Of_Order}@*
@xref{Parameters_Out_Of_Order}.

@item @code{Positional_Actuals_For_Defaulted_Generic_Parameters}@*
@xref{Positional_Actuals_For_Defaulted_Generic_Parameters}.

@item @code{Positional_Actuals_For_Defaulted_Parameters}@*
@xref{Positional_Actuals_For_Defaulted_Parameters}.

@item @code{Positional_Components}@*
@xref{Positional_Components}.

@item @code{Positional_Generic_Parameters}@*
@xref{Positional_Generic_Parameters}.

@item @code{Positional_Parameters}@*
@xref{Positional_Parameters}.

@item @code{Predefined_Numeric_Types}@*
@xref{Predefined_Numeric_Types}.

@item @code{Raising_External_Exceptions}@*
@xref{Raising_External_Exceptions}.

@item @code{Raising_Predefined_Exceptions}@*
@xref{Raising_Predefined_Exceptions}.

@item @code{Separate_Numeric_Error_Handlers}@*
@xref{Separate_Numeric_Error_Handlers}.

@ignore
@item @code{Recursion}
@item @code{Side_Effect_Functions}
@end ignore

@item @code{Slices}@*
@xref{Slices}.

@item @code{Too_Many_Parents}@*
@xref{Too_Many_Parents}.

@item @code{Unassigned_OUT_Parameters}@*
@xref{Unassigned_OUT_Parameters}.

@item @code{Uncommented_BEGIN_In_Package_Bodies}@*
@xref{Uncommented_BEGIN_In_Package_Bodies}.

@item @code{Recursive_Subprograms}@*
@xref{Recursive_Subprograms}.

@item @code{Unconditional_Exits}@*
@xref{Unconditional_Exits}.

@item @code{Unconstrained_Array_Returns}@*
@xref{Unconstrained_Array_Returns}.

@item @code{Universal_Ranges}@*
@xref{Universal_Ranges}.

@item @code{Unnamed_Blocks_And_Loops}@*
@xref{Unnamed_Blocks_And_Loops}.

@ignore
@item @code{Unused_Subprograms}
@end ignore

@item @code{USE_PACKAGE_Clauses}@*
@xref{USE_PACKAGE_Clauses}.

@item @code{Visible_Components}@*
@xref{Visible_Components}.

@item @code{Volatile_Objects_Without_Address_Clauses}@*
@xref{Volatile_Objects_Without_Address_Clauses}.

@end itemize



@c **********************************
@c * GNU Free Documentation License *
@c **********************************
@include gfdl.texi
@c GNU Free Documentation License

@node Index,,GNU Free Documentation License, Top
@unnumbered Index

@printindex cp

@contents
@c Put table of contents at end, otherwise it precedes the "title page" in
@c the .txt version
@c Edit the pdf file to move the contents to the beginning, after the title
@c page

@bye
