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::
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 *********************************
OSDN Git Service
