|
|
|
@ -463,15 +463,6 @@ The gnatmem Tool
|
|
|
|
|
|
|
|
|
|
Verifying Properties Using gnatcheck
|
|
|
|
|
|
|
|
|
|
* 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::
|
|
|
|
|
|
|
|
|
|
Sample Bodies Using gnatstub
|
|
|
|
|
|
|
|
|
|
* Running gnatstub::
|
|
|
|
@ -17246,648 +17237,12 @@ 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.
|
|
|
|
|
through @command{gnatcheck} switches.
|
|
|
|
|
|
|
|
|
|
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 @ref{The GNAT Driver and Project Files}).
|
|
|
|
|
|
|
|
|
|
Invoking @command{gnatcheck} on the command line has the form:
|
|
|
|
|
|
|
|
|
|
@smallexample
|
|
|
|
|
@c $ gnatcheck @ovar{switches} @{@var{filename}@}
|
|
|
|
|
@c @r{[}^-files^/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^/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^/INCLUDE_DIRS=^} 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.
|
|
|
|
|
|
|
|
|
|
@menu
|
|
|
|
|
* 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::
|
|
|
|
|
@end menu
|
|
|
|
|
|
|
|
|
|
@node Format of the Report File
|
|
|
|
|
@section Format of the Report File
|
|
|
|
|
@cindex Report file (for @code{gnatcheck})
|
|
|
|
|
|
|
|
|
|
@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^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 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
|
|
|
|
|
|
|
|
|
|
@node General gnatcheck Switches
|
|
|
|
|
@section General @command{gnatcheck} Switches
|
|
|
|
|
|
|
|
|
|
@noindent
|
|
|
|
|
The following switches control the general @command{gnatcheck} behavior
|
|
|
|
|
|
|
|
|
|
@table @option
|
|
|
|
|
@c !sort!
|
|
|
|
|
@cindex @option{^-a^/ALL^} (@command{gnatcheck})
|
|
|
|
|
@item ^-a^/ALL^
|
|
|
|
|
Process all units including those with read-only ALI files such as
|
|
|
|
|
those from the GNAT Run-Time library.
|
|
|
|
|
|
|
|
|
|
@ifclear vms
|
|
|
|
|
@ignore
|
|
|
|
|
@cindex @option{-d} (@command{gnatcheck})
|
|
|
|
|
@item -d
|
|
|
|
|
Debug mode
|
|
|
|
|
@end ignore
|
|
|
|
|
|
|
|
|
|
@cindex @option{-dd} (@command{gnatcheck})
|
|
|
|
|
@item -dd
|
|
|
|
|
Progress indicator mode (for use in GPS).
|
|
|
|
|
@end ifclear
|
|
|
|
|
|
|
|
|
|
@cindex @option{^-h^/HELP^} (@command{gnatcheck})
|
|
|
|
|
@item ^-h^/HELP^
|
|
|
|
|
List the predefined and user-defined rules. For more details see
|
|
|
|
|
@ref{Predefined Rules}.
|
|
|
|
|
|
|
|
|
|
@cindex @option{^-l^/LOCS^} (@command{gnatcheck})
|
|
|
|
|
@item ^-l^/LOCS^
|
|
|
|
|
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^/LOG^} (@command{gnatcheck})
|
|
|
|
|
@item ^-log^/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^/DIAGNOSTIC_LIMIT^} (@command{gnatcheck})
|
|
|
|
|
@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 output.
|
|
|
|
|
|
|
|
|
|
@cindex @option{^-q^/QUIET^} (@command{gnatcheck})
|
|
|
|
|
@item ^-q^/QUIET^
|
|
|
|
|
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{^--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^
|
|
|
|
|
Print out execution time.
|
|
|
|
|
|
|
|
|
|
@cindex @option{^-v^/VERBOSE^} (@command{gnatcheck})
|
|
|
|
|
@item ^-v^/VERBOSE^
|
|
|
|
|
Verbose mode; @command{gnatcheck} generates version information and then
|
|
|
|
|
a trace of sources being processed.
|
|
|
|
|
|
|
|
|
|
@cindex @option{^-o ^/OUTPUT^} (@command{gnatcheck})
|
|
|
|
|
@item ^-o ^/OUTPUT=^@var{report_file}
|
|
|
|
|
Set name of report file file to @var{report_file} .
|
|
|
|
|
|
|
|
|
|
@end table
|
|
|
|
|
|
|
|
|
|
@node gnatcheck Rule Options
|
|
|
|
|
@section @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 ON.
|
|
|
|
|
|
|
|
|
|
@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^/HELP^} 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.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@node Adding the Results of Compiler Checks to gnatcheck Output
|
|
|
|
|
@section 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 (@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
|
|
|
|
|
@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
|
|
|
|
|
|
|
|
|
|
To disable a specific restriction check, use @code{-RStyle_Checks} 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.
|
|
|
|
|
|
|
|
|
|
@node Project-Wide Checks
|
|
|
|
|
@section Project-Wide Checks
|
|
|
|
|
@cindex Project-wide checks (for @command{gnatcheck})
|
|
|
|
|
|
|
|
|
|
@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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@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
|
|
|
|
|
@c (Jan 2007) Since the global rules are still under development and are not
|
|
|
|
|
@c documented, there is no point in explaining the difference between
|
|
|
|
|
@c global and local rules
|
|
|
|
|
@noindent
|
|
|
|
|
A rule in @command{gnatcheck} is either local or global.
|
|
|
|
|
A @emph{local rule} is a rule that applies to a well-defined section
|
|
|
|
|
of a program and that can be checked by analyzing only this section.
|
|
|
|
|
A @emph{global rule} requires analysis of some global properties of the
|
|
|
|
|
whole program (mostly related to the program call graph).
|
|
|
|
|
As of @value{NOW}, the implementation of global rules should be
|
|
|
|
|
considered to be at a preliminary stage. You can use the
|
|
|
|
|
@option{+GLOBAL} option to enable all the global rules, and the
|
|
|
|
|
@option{-GLOBAL} rule option to disable all the global rules.
|
|
|
|
|
|
|
|
|
|
All the global rules in the list below are
|
|
|
|
|
so indicated by marking them ``GLOBAL''.
|
|
|
|
|
This +GLOBAL and -GLOBAL options are not
|
|
|
|
|
included in the list of gnatcheck options above, because at the moment they
|
|
|
|
|
are considered as a temporary debug options.
|
|
|
|
|
|
|
|
|
|
@command{gnatcheck} performs rule checks for generic
|
|
|
|
|
instances only for global rules. This limitation may be relaxed in a later
|
|
|
|
|
release.
|
|
|
|
|
@end ignore
|
|
|
|
|
|
|
|
|
|
@noindent
|
|
|
|
|
The predefined rules implemented in @command{gnatcheck}
|
|
|
|
|
are described in a companion document,
|
|
|
|
|
@cite{GNATcheck Reference Manual -- Predefined Rules}.
|
|
|
|
|
The rule identifier is
|
|
|
|
|
used as a parameter of @command{gnatcheck}'s @option{+R} or @option{-R}
|
|
|
|
|
switches.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@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
|
|
|
|
|
For full details, refer to @cite{GNATcheck Reference Manual} document.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
@c *********************************
|
|
|
|
|