The Cross-Referencing Tools gnatxref and gnatfind
-* gnatxref Switches::
-* gnatfind Switches::
+* Switches for gnatxref::
+* Switches for gnatfind::
* Project Files for gnatxref and gnatfind::
* Regular Expressions in gnatfind and gnatxref::
* Examples of gnatxref Usage::
* gnatcheck Rule Options::
* Adding the Results of Compiler Checks to gnatcheck Output::
* Project-Wide Checks::
+* Rule exemption::
* Predefined Rules::
+* Example of gnatcheck Usage::
Sample Bodies Using gnatstub
@item -gnatB
@cindex @option{-gnatB} (@command{gcc})
-Assume no invalid (bad) values except for 'Valid attribute use.
+Assume no invalid (bad) values except for 'Valid attribute use
+(@pxref{Validity Checking}).
@item -gnatc
@cindex @option{-gnatc} (@command{gcc})
@end ifclear
(@pxref{Integrated Preprocessing}).
+@item -gnateS
+@cindex @option{-gnateS} (@command{gcc})
+Generate SCO (Source Coverage Obligation) information in the ALI
+file. This information is used by advanced coverage tools. See
+unit @file{SCOs} in the compiler sources for details in files
+@file{scos.ads} and @file{scos.adb}.
+
@item -gnatE
@cindex @option{-gnatE} (@command{gcc})
Full dynamic elaboration checks.
@item -gnatV
@cindex @option{-gnatV} (@command{gcc})
-Control level of validity checking. See separate section describing
-this feature.
+Control level of validity checking (@pxref{Validity Checking}).
@item ^-gnatw@var{xxx}^/WARNINGS=(@var{option}@r{[},@dots{}@r{]})^
@cindex @option{^-gnatw^/WARNINGS^} (@command{gcc})
@item
The switches
-@option{^-gnatz^/DISTRIBUTION_STUBS^}, @option{-gnatzc}, and @option{-gnatzr}
-may not be combined with any other switches.
+^^@option{/DISTRIBUTION_STUBS=},^
+@option{-gnatzc} and @option{-gnatzr} may not be combined with any other
+switches, and only one of them may appear in the command line.
@ifclear vms
@item
@item
Once a ``V'' appears in the string (that is a use of the @option{-gnatV}
switch), then all further characters in the switch are interpreted
-as validity checking options (see description of @option{-gnatV}).
+as validity checking options (@pxref{Validity Checking}).
+
+@item
+Option ``em'', ``ec'', ``ep'', ``l='' and ``R'' must be the last options in
+a combined list of options.
@end ifclear
@end itemize
This switch disables warnings for a @code{with} of an internal GNAT
implementation unit.
+@item -gnatw.i
+@emph{Activate warnings on overlapping actuals.}
+@cindex @option{-gnatw.i} (@command{gcc})
+This switch enables a warning on statically detectable overlapping actuals in
+a subprogram call, when one of the actuals is an in-out parameter, and the
+types of the actuals are not by-copy types. The warning is off by default,
+and is not included under -gnatwa.
+
+@item -gnatw.I
+@emph{Disable warnings on overlapping actuals.}
+@cindex @option{-gnatw.I} (@command{gcc})
+This switch disables warnings on overlapping actuals in a call..
+
@item -gnatwj
@emph{Activate warnings on obsolescent features (Annex J).}
@cindex @option{-gnatwj} (@command{gcc})
@findex Validity Checking
@noindent
-The Ada Reference Manual has specific requirements for checking
-for invalid values. In particular, RM 13.9.1 requires that the
-evaluation of invalid values (for example from unchecked conversions),
-not result in erroneous execution. In GNAT, the result of such an
-evaluation in normal default mode is to either use the value
-unmodified, or to raise Constraint_Error in those cases where use
-of the unmodified value would cause erroneous execution. The cases
-where unmodified values might lead to erroneous execution are case
-statements (where a wild jump might result from an invalid value),
-and subscripts on the left hand side (where memory corruption could
-occur as a result of an invalid value).
+The Ada Reference Manual defines the concept of invalid values (see
+RM 13.9.1). The primary source of invalid values is uninitialized
+variables. A scalar variable that is left uninitialized may contain
+an invalid value; the concept of invalid does not apply to access or
+composite types.
+
+It is an error to read an invalid value, but the RM does not require
+run-time checks to detect such errors, except for some minimal
+checking to prevent erroneous execution (i.e. unpredictable
+behavior). This corresponds to the @option{-gnatVd} switch below,
+which is the default. For example, by default, if the expression of a
+case statement is invalid, it will raise Constraint_Error rather than
+causing a wild jump, and if an array index on the left-hand side of an
+assignment is invalid, it will raise Constraint_Error rather than
+overwriting an arbitrary memory location.
+
+The @option{-gnatVa} may be used to enable additional validity checks,
+which are not required by the RM. These checks are often very
+expensive (which is why the RM does not require them). These checks
+are useful in tracking down uninitialized variables, but they are
+not usually recommended for production builds.
+
+The other @option{-gnatV^@var{x}^^} switches below allow finer-grained
+control; you can enable whichever validity checks you desire. However,
+for most debugging purposes, @option{-gnatVa} is sufficient, and the
+default @option{-gnatVd} (i.e. standard Ada behavior) is usually
+sufficient for non-debugging use.
The @option{-gnatB} switch tells the compiler to assume that all
values are valid (that is, within their declared subtype range)
except in the context of a use of the Valid attribute. This means
the compiler can generate more efficient code, since the range
-of values is better known at compile time.
+of values is better known at compile time. However, an uninitialized
+variable can cause wild jumps and memory corruption in this mode.
-The @option{-gnatV^@var{x}^^} switch allows more control over the validity
-checking mode.
+The @option{-gnatV^@var{x}^^} switch allows control over the validity
+checking mode as described below.
@ifclear vms
The @code{x} argument is a string of letters that
indicate validity checks that are performed or not performed in addition
-to the default checks described above.
+to the default checks required by Ada as described above.
@end ifclear
@ifset vms
The options allowed for this qualifier
indicate validity checks that are performed or not performed in addition
-to the default checks described above.
+to the default checks required by Ada as described above.
@end ifset
@table @option
a space must separate the two tokens.
@item
+if the token following a right parenthesis starts with a letter or digit, then
+a space must separate the two tokens.
+
+@item
A right parenthesis must either be the first non-blank character on
a line, or it must be preceded by a non-blank character.
XTRA_PARENS, and DOS_LINE_ENDINGS. In addition
@end ifset
-
-
The switch
@ifclear vms
@option{-gnatyN}
@table @option
-@item -gnatem^^=^@var{path}
+@item -gnatem=@var{path}
@cindex @option{-gnatem} (@command{gcc})
A mapping file is a way to communicate to the compiler two mappings:
from unit names to file names (without any directory information) and from
sources are read over a slow network connection. In normal operation,
you need not be concerned with the format or use of mapping files,
and the @option{-gnatem} switch is not a switch that you would use
-explicitly. it is intended only for use by automatic tools such as
+explicitly. It is intended primarily for use by automatic tools such as
@command{gnatmake} running under the project file facility. The
description here of the format of mapping files is provided
for completeness and for possible use by other tools.
-A mapping file is a sequence of sets of three lines. In each set,
-the first line is the unit name, in lower case, with ``@code{%s}''
-appended for
-specs and ``@code{%b}'' appended for bodies; the second line is the
+A mapping file is a sequence of sets of three lines. In each set, the
+first line is the unit name, in lower case, with @code{%s} appended
+for specs and @code{%b} appended for bodies; the second line is the
file name; and the third line is the path name.
Example:
/gnat/project1/sources/main.2.ada
@end smallexample
-When the switch @option{-gnatem} is specified, the compiler will create
-in memory the two mappings from the specified file. If there is any problem
-(nonexistent file, truncated file or duplicate entries), no mapping will
-be created.
+When the switch @option{-gnatem} is specified, the compiler will
+create in memory the two mappings from the specified file. If there is
+any problem (nonexistent file, truncated file or duplicate entries),
+no mapping will be created.
-Several @option{-gnatem} switches may be specified; however, only the last
-one on the command line will be taken into account.
+Several @option{-gnatem} switches may be specified; however, only the
+last one on the command line will be taken into account.
-When using a project file, @command{gnatmake} create a temporary mapping file
-and communicates it to the compiler using this switch.
+When using a project file, @command{gnatmake} creates a temporary
+mapping file and communicates it to the compiler using this switch.
@end table
@item ^-C^/MAPPING^
@cindex @option{^-C^/MAPPING^} (@command{gnatmake})
-Use a temporary mapping file. A mapping file is a way to communicate to the
-compiler two mappings: from unit names to file names (without any directory
-information) and from file names to path names (with full directory
-information). These mappings are used by the compiler to short-circuit the path
-search. When @command{gnatmake} is invoked with this switch, it will create
-a temporary mapping file, initially populated by the project manager,
-if @option{^-P^/PROJECT_FILE^} is used, otherwise initially empty.
-Each invocation of the compiler will add the newly accessed sources to the
-mapping file. This will improve the source search during the next invocation
-of the compiler.
+Use a temporary mapping file. A mapping file is a way to communicate
+to the compiler two mappings: from unit names to file names (without
+any directory information) and from file names to path names (with
+full directory information). A mapping file can make the compiler's
+file searches faster, especially if there are many source directories,
+or the sources are read over a slow network connection. If
+@option{^-P^/PROJECT_FILE^} is used, a mapping file is always used, so
+@option{^-C^/MAPPING^} is unnecessary; in this case the mapping file
+is initially populated based on the project file. If
+@option{^-C^/MAPPING^} is used without
+@option{^-P^/PROJECT_FILE^},
+the mapping file is initially empty. Each invocation of the compiler
+will add any newly accessed sources to the mapping file.
@item ^-C=^/USE_MAPPING_FILE=^@var{file}
@cindex @option{^-C=^/USE_MAPPING^} (@command{gnatmake})
@ifclear vms
@item -eL
@cindex @option{-eL} (@command{gnatmake})
+@cindex symbolic links
Follow all symbolic links when processing project files.
+This should be used if your project uses symbolic links for files or
+directories, but is not needed in other cases.
+
+@cindex naming scheme
+This also assumes that no directory matches the naming scheme for files (for
+instance that you do not have a directory called "sources.ads" when using the
+default GNAT naming scheme).
+
+When you do not have to use this switch (ie by default), gnatmake is able to
+save a lot of system calls (several per source file and object file), which
+can result in a significant speed up to load and manipulate a project file,
+especially when using source files from a remote system.
+
@end ifclear
@item ^-eS^/STANDARD_OUTPUT_FOR_COMMANDS^
@item
@code{Cross_Reference}
@item
+@code{Check}
+@item
@code{Eliminate}
@item
@code{Pretty_Printer}
package @code{Linker} for command LINK (invoking @code{^gnatlink^gnatlink^})
@item
+package @code{Check} for command CHECK
+(invoking @code{^gnatcheck^gnatcheck^})
+
+@item
package @code{Metrics} for command METRIC
(invoking @code{^gnatmetric^gnatmetric^})
use the @code{gnat} driver (see @ref{The GNAT Driver and Project Files}).
@menu
-* gnatxref Switches::
-* gnatfind Switches::
+* Switches for gnatxref::
+* Switches for gnatfind::
* Project Files for gnatxref and gnatfind::
* Regular Expressions in gnatfind and gnatxref::
* Examples of gnatxref Usage::
* Examples of gnatfind Usage::
@end menu
-@node gnatxref Switches
+@node Switches for gnatxref
@section @code{gnatxref} Switches
@noindent
you can say @samp{gnatxref ^-ag^/ALL_FILES/IGNORE_LOCALS^} instead of
@samp{gnatxref ^-a -g^/ALL_FILES /IGNORE_LOCALS^}.
-@node gnatfind Switches
+@node Switches for gnatfind
@section @code{gnatfind} Switches
@noindent
@cindex @option{-nostdlib} (@command{gnatfind})
Do not look for library files in the system default directory.
+@item --ext=@var{extension}
+@cindex @option{--ext} (@command{gnatfind})
+Specify an alternate ali file extension. The default is @code{ali} and other
+extensions (e.g. @code{sli} for SPARK library files) may be specified via this
+switch. Note that if this switch overrides the default, which means that only
+the new extension will be considered.
+
@item --RTS=@var{rts-path}
@cindex @option{--RTS} (@command{gnatfind})
Specifies the default location of the runtime library. Same meaning as the
Do not place the keyword @code{is} on a separate line in a subprogram body in
case if the spec occupies more then one line.
+@cindex @option{^--separate-label^/SEPARATE_LABEL^} (@command{gnatpp})
+@item ^--separate-label^/SEPARATE_LABEL^
+Place statement label(s) on a separate line, with the following statement
+on the next line.
+
@cindex @option{^--separate-loop-then^/SEPARATE_LOOP_THEN^} (@command{gnatpp})
@item ^--separate-loop-then^/SEPARATE_LOOP_THEN^
Place the keyword @code{loop} in FOR and WHILE loop statements and the
Here is an example of simple library interface for use with C main program:
@smallexample @c ada
-package Interface is
+package My_Package is
procedure Do_Something;
pragma Export (C, Do_Something, "do_something");
procedure Do_Something_Else;
pragma Export (C, Do_Something_Else, "do_something_else");
-end Interface;
+end My_Package;
@end smallexample
@noindent
@smallexample
$ gnatcheck @ovar{switches} @{@var{filename}@}
@r{[}^-files^/FILES^=@{@var{arg_list_filename}@}@r{]}
- @r{[}-cargs @var{gcc_switches}@r{]} @r{[}-rules @var{rule_options}@r{]}
+ @r{[}-cargs @var{gcc_switches}@r{]} -rules @var{rule_options}
@end smallexample
@noindent
@end itemize
@noindent
-Either a @file{@var{filename}} or an @file{@var{arg_list_filename}} must be supplied.
+Either a @file{@var{filename}} or an @file{@var{arg_list_filename}} must be
+supplied.
@menu
* Format of the Report File::
* gnatcheck Rule Options::
* Adding the Results of Compiler Checks to gnatcheck Output::
* Project-Wide Checks::
+* Rule exemption::
* Predefined Rules::
+* Example of gnatcheck Usage::
@end menu
@node Format of the Report File
The @command{gnatcheck} tool outputs on @file{stdout} all messages concerning
rule violations.
It also creates a text file that
-contains the complete report of the last gnatcheck run. By default this file is
-named named @file{^gnatcheck.out^GNATCHECK.OUT^} and it is located in the current
-directory, @option{^-o^/OUTPUT^} option can be used to change the name and/or
-location of the report file. This report contains:
+contains the complete report of the last gnatcheck run. By default this file
+is named named @file{^gnatcheck.out^GNATCHECK.OUT^} and it is located in the
+current directory; the @option{^-o^/OUTPUT^} option can be used to change the
+name and/or location of the report file. This report contains:
@itemize @bullet
-@item a list of the Ada source files being checked,
-@item a list of enabled and disabled rules,
-@item a list of the diagnostic messages, ordered in three different ways
-and collected in three separate
-sections. Section 1 contains the raw list of diagnostic messages. It
-corresponds to the output going to @file{stdout}. Section 2 contains
-messages ordered by rules.
-Section 3 contains messages ordered by source files.
+@item date and time of @command{gnatcheck} run, the version of
+the tool that has generated this report and the full parameters
+of the @command{gnatcheck} invocation;
+@item list of enabled rules;
+@item total number of detected violations;
+@item list of source files where rule violations have been detected;
+@item list of source files where no violations have been detected.
@end itemize
@node General gnatcheck Switches
@cindex @option{^-a^/ALL^} (@command{gnatcheck})
@item ^-a^/ALL^
Process all units including those with read-only ALI files such as
-those from GNAT Run-Time library.
+those from the GNAT Run-Time library.
@ifclear vms
@ignore
@cindex @option{-dd} (@command{gnatcheck})
@item -dd
-Progress indicator mode (for use in GPS)
+Progress indicator mode (for use in GPS).
@end ifclear
@cindex @option{^-h^/HELP^} (@command{gnatcheck})
@cindex @option{^-log^/LOG^} (@command{gnatcheck})
@item ^-log^/LOG^
-Duplicate all the output sent to Stderr into a log file. The log file is
-named @var{gnatcheck.log} and is located in the current directory.
+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^/DIAGNOSTIC_LIMIT^} (@command{gnatcheck})
-@item ^-m@i{nnn}^/DIAGNOSTIC_LIMIT=@i{nnn}^
-Maximum number of diagnoses to be sent to Stdout, @i{nnn} from o@dots{}1000,
+@item ^-m@i{nnnn}^/DIAGNOSTIC_LIMIT=@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 printed into Stdout.
+the number of diagnostic messages to be output.
@cindex @option{^-q^/QUIET^} (@command{gnatcheck})
@item ^-q^/QUIET^
-Quiet mode. All the diagnoses about rule violations are placed in the
-@command{gnatcheck} report file only, without duplicating in @file{stdout}.
+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^/SHORT^} (@command{gnatcheck})
@item ^-s^/SHORT^
Short format of the report file (no version information, no list of applied
rules, no list of checked sources is included)
-@cindex @option{^-s1^/COMPILER_STYLE^} (@command{gnatcheck})
-@item ^-s1^/COMPILER_STYLE^
-Include the compiler-style section in the report file
-
-@cindex @option{^-s2^/BY_RULES^} (@command{gnatcheck})
-@item ^-s2^/BY_RULES^
-Include the section containing diagnoses ordered by rules in the report file
-
-@cindex @option{^-s3^/BY_FILES_BY_RULES^} (@command{gnatcheck})
-@item ^-s3^/BY_FILES_BY_RULES^
-Include the section containing diagnoses ordered by files and then by rules
-in the report file
+@cindex @option{^--include-file=@var{file}^/INCLUDE_FILE=@var{file}^} (@command{gnatcheck})
+@item ^--include-file^/INCLUDE_FILE^
+Append the content of the specified text file to the report file
@cindex @option{^-t^/TIME^} (@command{gnatcheck})
@item ^-t^/TIME^
@cindex @option{-from} (@command{gnatcheck})
@item -from=@var{rule_option_filename}
-Read the rule options from the text file @var{rule_option_filename}, referred as
-``rule file'' below.
+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.
-A rule file is a text file containing a set of rule options.
-@cindex Rule file (for @code{gnatcheck})
+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). The rule file has free format; that is,
-you do not have to start a new rule option on a new line.
+lines and end-of-line comments). There can be several rule options on a
+single line (separated by a space).
-A rule file may contain other @option{-from=@var{rule_option_filename}}
+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 rule file during the rule files processing. In case a
+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}}),
-the processing of rule files is interrupted and a part of their content
-is ignored.
+processing fails with an error message.
@node Adding the Results of Compiler Checks to gnatcheck Output
@table @option
@item Restrictions
-To record restrictions violations (that are performed by the compiler if the
+To record restrictions violations (which are performed by the compiler if the
pragma @code{Restrictions} or @code{Restriction_Warnings} are given),
-use the rule named
-@code{Restrictions} with the same parameters as pragma
+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(@pxref{Style Checking}), use the rule named
-@code{Style_Checks}. A parameter of this rule can be either @code{All_Checks},
-which enables all the standard style checks that corresponds to @option{-gnatyy}
-GNAT style check option, or a string that has exactly the same
-structure and semantics as the @code{string_LITERAL} parameter of GNAT pragma
-@code{Style_Checks} (for further information about this pragma,
-@pxref{Pragma Style_Checks,,, gnat_rm, GNAT Reference Manual}). For example,
-@code{+RStyle_Checks:O} rule option activates and adds to @command{gnatcheck}
-output the compiler style check that corresponds to
+To record compiler style checks (@pxref{Style Checking}), 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 (@pxref{Warning Message Control}), use the rule
-named @code{Warnings} with a parameter that is a valid
-@i{static_string_expression} argument of GNAT pragma @code{Warnings}
-(for further information about this pragma, @pxref{Pragma Warnings,,,
-gnat_rm, GNAT Reference Manual}). Note, that in case of gnatcheck
+To record compiler warnings (@pxref{Warning Message Control}), 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
@end smallexample
+@node Rule exemption
+@section Rule exemption
+@cindex Rule exemption (for @command{gnatcheck})
+
+@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
+@subsection 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.
+
+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
+@subsection @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
+
+
@node Predefined Rules
@section Predefined Rules
@cindex Predefined rules (for @command{gnatcheck})
@ignore
* Ceiling_Violations::
@end ignore
+* Complex_Inlined_Subprograms::
* Controlled_Type_Declarations::
* Declarations_In_Blocks::
+* Deep_Inheritance_Hierarchies::
+* Deeply_Nested_Generics::
+* Deeply_Nested_Inlining::
+@ignore
+* Deeply_Nested_Local_Inlining::
+@end ignore
* Default_Parameters::
+* Direct_Calls_To_Primitives::
* Discriminated_Records::
* Enumeration_Ranges_In_CASE_Statements::
* Exceptions_As_Control_Flow::
* Expanded_Loop_Exit_Names::
* Explicit_Full_Discrete_Ranges::
* Float_Equality_Checks::
+* Forbidden_Attributes::
* Forbidden_Pragmas::
* Function_Style_Procedures::
* Generics_In_Subprograms::
* Improperly_Called_Protected_Entries::
@end ignore
* Metrics::
+* Misnamed_Controlling_Parameters::
* Misnamed_Identifiers::
* Multiple_Entries_In_Protected_Definitions::
* Name_Clashes::
* Side_Effect_Functions::
@end ignore
* Slices::
+* Too_Many_Parents::
* Unassigned_OUT_Parameters::
* Uncommented_BEGIN_In_Package_Bodies::
* Unconditional_Exits::
* Unused_Subprograms::
@end ignore
* USE_PACKAGE_Clauses::
+* Visible_Components::
* Volatile_Objects_Without_Address_Clauses::
@end menu
@cindex @code{Anonymous_Subtypes} rule (for @command{gnatcheck})
@noindent
-Flag all uses of anonymous subtypes. A use of an anonymous subtype is
+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
@ignore
@node Ceiling_Violations
-@subsection @code{Ceiling_Violations} (under construction, GLOBAL)
+@subsection @code{Ceiling5_Violations} (under construction, GLOBAL)
@cindex @code{Ceiling_Violations} rule (for @command{gnatcheck})
@noindent
This rule has no parameters.
+@node Complex_Inlined_Subprograms
+@subsection @code{Complex_Inlined_Subprograms}
+@cindex @code{Complex_Inlined_Subprograms} rule (for @command{gnatcheck})
+
+@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 Declarations_In_Blocks
@subsection @code{Declarations_In_Blocks}
This rule has no parameters.
+@node Deep_Inheritance_Hierarchies
+@subsection @code{Deep_Inheritance_Hierarchies}
+@cindex @code{Deep_Inheritance_Hierarchies} rule (for @command{gnatcheck})
+
+@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 Deeply_Nested_Generics
+@subsection @code{Deeply_Nested_Generics}
+@cindex @code{Deeply_Nested_Generics} rule (for @command{gnatcheck})
+
+@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 declaratons 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 Deeply_Nested_Inlining
+@subsection @code{Deeply_Nested_Inlining}
+@cindex @code{Deeply_Nested_Inlining} rule (for @command{gnatcheck})
+
+@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
+
+
+@ignore
+@node Deeply_Nested_Local_Inlining
+@subsection @code{Deeply_Nested_Local_Inlining}
+@cindex @code{Deeply_Nested_Local_Inlining} rule (for @command{gnatcheck})
+
+@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 inlided, 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 usefull for the case
+when neiter @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
+
@node Default_Parameters
@subsection @code{Default_Parameters}
@cindex @code{Default_Parameters} rule (for @command{gnatcheck})
This rule has no parameters.
+@node Direct_Calls_To_Primitives
+@subsection @code{Direct_Calls_To_Primitives}
+@cindex @code{Direct_Calls_To_Primitives} rule (for @command{gnatcheck})
+
+@noindent
+Flags any non-dispatching call to a dispatching primitive operation, except
+for the common idiom where a primitive subprogram for a tagged type
+directly calls the same primitive subprogram of the type's immediate ancestor.
+
+This rule has no parameters.
+
+
@node Discriminated_Records
@subsection @code{Discriminated_Records}
@cindex @code{Discriminated_Records} rule (for @command{gnatcheck})
This rule has no parameters.
+@node Forbidden_Attributes
+@subsection @code{Forbidden_Attributes}
+@cindex @code{Forbidden_Attributes} rule (for @command{gnatcheck})
+
+@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
@subsection @code{Forbidden_Pragmas}
@cindex @code{Forbidden_Pragmas} rule (for @command{gnatcheck})
-RMetrics_Cyclomatic_Complexity
@end smallexample
+
+@node Misnamed_Controlling_Parameters
+@subsection @code{Misnamed_Controlling_Parameters}
+@cindex @code{Misnamed_Controlling_Parameters} rule (for @command{gnatcheck})
+
+@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
@subsection @code{Misnamed_Identifiers}
@cindex @code{Misnamed_Identifiers} rule (for @command{gnatcheck})
@end itemize
@noindent
-For a private or incomplete type declaration the following checks are
-made for the defining name suffix:
-
-@itemize @bullet
-@item
-For an incomplete type declaration: if the corresponding full type
-declaration is available, the defining identifier from the full type
-declaration is checked, but the defining identifier from the incomplete type
-declaration is not; otherwise the defining identifier from the incomplete
-type declaration is checked against the suffix specified for type
-declarations.
+Defining identifiers from incomplete type declarations are never flagged.
-@item
-For a private type declaration (including private extensions), the defining
+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.
-@end itemize
@noindent
For a deferred constant, the defining name in the corresponding full constant
@cindex @code{Positional_Generic_Parameters} rule (for @command{gnatcheck})
@noindent
-Flag each instantiation using positional parameter notation.
+Flag each positional actual generic parameter except for the case when
+the generic unit being iinstantiated has exactly one generic formal
+parameter.
This rule has no parameters.
@cindex @code{Positional_Parameters} rule (for @command{gnatcheck})
@noindent
-Flag each subprogram or entry call using positional parameter notation,
+Flag each positional parameter notation in a subprogram or entry call,
except for the following:
@itemize @bullet
@item
-Invocations of prefix or infix operators are not flagged
+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 call is not flagged;
+the parameter of the call is not flagged;
@item
If a subprogram call uses the @emph{Object.Operation} notation, then
@itemize @minus
This rule has no parameters.
+@node Too_Many_Parents
+@subsection @code{Too_Many_Parents}
+@cindex @code{Too_Many_Parents} rule (for @command{gnatcheck})
+
+@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 Unassigned_OUT_Parameters
@subsection @code{Unassigned_OUT_Parameters}
@cindex @code{Unassigned_OUT_Parameters} rule (for @command{gnatcheck})
Flag each function returning an unconstrained array. Function declarations,
function bodies (and body stubs) having no separate specifications,
and generic function instantiations are checked.
-Generic function declarations, function calls and function renamings are
+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 no parameters.
@node Universal_Ranges
This rule has no parameters.
+@node Visible_Components
+@subsection @code{Visible_Components}
+@cindex @code{Visible_Components} rule (for @command{gnatcheck})
+
+@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.
+
@node Volatile_Objects_Without_Address_Clauses
@subsection @code{Volatile_Objects_Without_Address_Clauses}
This rule has no parameters.
+@node Example of gnatcheck Usage
+@section 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 *********************************
@node Creating Sample Bodies Using gnatstub
For GNAT running on other than VMS systems, all the HP Ada 83 pragmas and
attributes are recognized, although only a subset of them can sensibly
be implemented. The description of pragmas in
-@xref{Implementation Defined Pragmas,,, gnat_rm, GNAT Reference Manual}
+@xref{Implementation Defined Pragmas,,, gnat_rm, GNAT Reference Manual},
indicates whether or not they are applicable to non-VMS systems.
@menu
@noindent
The pragma @code{Extend_System} is a configuration pragma that
is most conveniently placed in the @file{gnat.adc} file. @xref{Pragma
-Extend_System,,, gnat_rm, GNAT Reference Manual} for further details.
+Extend_System,,, gnat_rm, GNAT Reference Manual}, for further details.
HP Ada does not allow the recompilation of the package
@code{SYSTEM}. Instead HP Ada provides several pragmas
@code{TO_ADDRESS}
function for type @code{UNSIGNED_LONGWORD} is changed to
@code{TO_ADDRESS_LONG}.
-@xref{Address Clauses,,, gnat_rm, GNAT Reference Manual} for a
+@xref{Address Clauses,,, gnat_rm, GNAT Reference Manual}, for a
discussion of why this change was necessary.
@noindent
OSDN Git Service
