| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
gnatcheck
The gnatcheck tool is an ASIS-based utility that checks properties
of Ada source files according to a given set of semantic rules.
In order to check compliance with a given rule, gnatcheck has to
semantically analyze the Ada sources.
Therefore, checks can only be performed on
legal Ada units. Moreover, when a unit depends semantically upon units located
outside the current directory, the source search path has to be provided when
calling gnatcheck, either through a specified project file or
through gnatcheck switches as described below.
A number of rules are predefined in gnatcheck and are described
later in this chapter.
You can also add new rules, by modifying the gnatcheck code and
rebuilding the tool. In order to add a simple rule making some local checks,
a small amount of straightforward ASIS-based programming is usually needed.
Project support for gnatcheck is provided by the GNAT
driver (see 12.2 The GNAT Driver and Project Files).
Invoking gnatcheck on the command line has the form:
$ gnatcheck [switches] {filename}
[-files={arg_list_filename}]
[-cargs gcc_switches] -rules rule_options
|
where
gcc. They will be passed on to all compiler invocations made by
gnatcheck to generate the ASIS trees. Here you can provide
`-I' switches to form the source search path,
and use the `-gnatec' switch to set the configuration file.
gnatcheck (see section 24.3 gnatcheck Rule Options).
Either a `filename' or an `arg_list_filename' must be supplied.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The gnatcheck tool outputs on `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 `gnatcheck.out' and it is located in the
current directory; the `-o' option can be used to change the
name and/or location of the report file. This report contains:
gnatcheck run, the version of
the tool that has generated this report and the full parameters
of the gnatcheck invocation;
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
gnatcheck Switches
The following switches control the general gnatcheck behavior
gnatcheck report file only, without duplication on `stdout'.
gnatcheck generates version information and then
a trace of sources being processed.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
gnatcheck Rule Options
The following options control the processing performed by
gnatcheck.
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. The file may contain empty lines and Ada-style comments (comment lines and end-of-line comments). There can be several rule options on a single line (separated by a space).
A coding standard file may reference other coding standard files by including more `-from=rule_option_filename' options, each such option being replaced with the content of the corresponding coding standard file during processing. In case a cycle is detected (that is, `rule_file_1' reads rule options from `rule_file_2', and `rule_file_2' reads (directly or indirectly) rule options from `rule_file_1'), processing fails with an error message.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
gnatcheck Output
The gnatcheck tool can include in the generated diagnostic messages
and in
the report file the results of the checks performed by the compiler. Though
disabled by default, this effect may be obtained by using `+R' with
the following rule identifiers and parameters:
Restrictions or Restriction_Warnings are given),
use the Restrictions rule
with the same parameters as pragma
Restrictions or Restriction_Warnings.
Style_Checks rule.
This rule takes a parameter in one of the following forms:
All_Checks,
which enables the standard style checks corresponding to the `-gnatyy'
GNAT style check option, or
string_LITERAL parameter of the
GNAT pragma Style_Checks
(for further information about this pragma,
see section `Pragma Style_Checks' in GNAT Reference Manual).
For example, the
+RStyle_Checks:O rule option activates
the compiler style check that corresponds to
-gnatyO style check option.
Warnings rule with a parameter that is a valid
static_string_expression argument of the GNAT pragma Warnings
(for further information about this pragma,
see section `Pragma Warnings' in GNAT Reference Manual).
Note that in case of gnatcheck
's' parameter, that corresponds to the GNAT `-gnatws' option, disables
all the specific warnings, but not suppresses the warning mode,
and 'e' parameter, corresponding to `-gnatwe' that means
"treat warnings as errors", does not have any effect.
To disable a specific restriction check, use -RStyle_Checks gnatcheck
option with the corresponding restriction name as a parameter. -R is
not available for Style_Checks and Warnings options, to disable
warnings and style checks, use the corresponding warning and style options.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
In order to perform checks on all units of a given project, you can use the GNAT driver along with the `-P' option:
gnat check -Pproj -rules -from=my_rules |
If the project proj depends upon other projects, you can perform
checks on the project closure using the `-U' option:
gnat check -Pproj -U -rules -from=my_rules |
Finally, if not all the units are relevant to a particular main program in the project closure, you can perform checks for the set of units needed to create a given main program (unit closure) using the `-U' option followed by the name of the main unit:
gnat check -Pproj -U main -rules -from=my_rules |
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
One of the most useful applications of gnatcheck is to
automate the enforcement of project-specific coding standards,
for example in safety-critical systems where particular features
must be restricted in order to simplify the certification effort.
However, it may sometimes be appropriate to violate a coding standard rule,
and in such cases the rationale for the violation should be provided
in the source program itself so that the individuals
reviewing or maintaining the program can immediately understand the intent.
The gnatcheck tool supports this practice with the notion of
a "rule exemption" covering a specific source code section. Normally
rule violation messages are issued both on `stderr'
and in a report file. In contrast, exempted violations are not listed on
`stderr'; thus users invoking gnatcheck interactively
(e.g. in its GPS interface) do not need to pay attention to known and
justified violations. However, exempted violations along with their
justification are documented in a special section of the report file that
gnatcheck generates.
24.6.1 Using pragma Annotateto Control Rule Exemption24.6.2 gnatcheckAnnotations Rules
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Annotate to Control Rule Exemption
Rule exemption is controlled by pragma Annotate when its first
argument is "gnatcheck". The syntax of gnatcheck's
exemption control annotations is as follows:
pragma Annotate (gnatcheck, exemption_control, Rule_Name, [justification]); exemption_control ::= Exempt_On | Exempt_Off Rule_Name ::= string_literal justification ::= string_literal |
When a gnatcheck annotation has more then four arguments,
gnatcheck issues a warning and ignores the additional arguments.
If the additional arguments do not follow the syntax above,
gnatcheck emits a warning and ignores the annotation.
The Rule_Name argument should be the name of some existing
gnatcheck rule.
Otherwise a warning message is generated and the pragma is
ignored. If Rule_Name denotes a rule that is not activated by the given
gnatcheck call, the pragma is ignored and no warning is issued.
A source code section where an exemption is active for a given rule is
delimited by an exempt_on and exempt_off annotation pair:
pragma Annotate (gnatcheck, Exempt_On, Rule_Name, "justification"); -- source code section pragma Annotate (gnatcheck, Exempt_Off, Rule_Name); |
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
gnatcheck Annotations Rules
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The predefined rules implemented in gnatcheck
are described in a companion document,
GNATcheck Reference Manual -- Predefined Rules.
The rule identifier is
used as a parameter of gnatcheck's `+R' or `-R'
switches.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
gnatcheck Usage Here is a simple example. Suppose that in the current directory we have a project file named `gnatcheck_example.gpr' with the following content:
project Gnatcheck_Example is
for Source_Dirs use ("src");
for Object_Dir use "obj";
for Main use ("main.adb");
package Check is
for Default_Switches ("ada") use ("-rules", "-from=coding_standard");
end Check;
end Gnatcheck_Example;
|
And the file named `coding_standard' is also located in the current directory and has the following content:
----------------------------------------------------- -- This is a sample gnatcheck coding standard file -- ----------------------------------------------------- -- First, turning on rules, that are directly implemented in gnatcheck +RAbstract_Type_Declarations +RAnonymous_Arrays +RLocal_Packages +RFloat_Equality_Checks +REXIT_Statements_With_No_Loop_Name -- Then, activating compiler checks of interest: +RStyle_Checks:e -- This style check checks if a unit name is present on END keyword that -- is the end of the unit declaration |
And the subdirectory `src' contains the following Ada sources:
`pack.ads':
package Pack is
type T is abstract tagged private;
procedure P (X : T) is abstract;
package Inner is
type My_Float is digits 8;
function Is_Equal (L, R : My_Float) return Boolean;
end Inner;
private
type T is abstract tagged null record;
end;
|
`pack.adb':
package body Pack is
package body Inner is
function Is_Equal (L, R : My_Float) return Boolean is
begin
return L = R;
end;
end Inner;
end Pack;
|
and `main.adb'
with Pack; use Pack;
procedure Main is
pragma Annotate
(gnatcheck, Exempt_On, "Anonymous_Arrays", "this one is fine");
Float_Array : array (1 .. 10) of Inner.My_Float;
pragma Annotate (gnatcheck, Exempt_Off, "Anonymous_Arrays");
Another_Float_Array : array (1 .. 10) of Inner.My_Float;
use Inner;
B : Boolean := False;
begin
for J in Float_Array'Range loop
if Is_Equal (Float_Array (J), Another_Float_Array (J)) then
B := True;
exit;
end if;
end loop;
end Main;
|
And suppose we call gnatcheck from the current directory using
the gnat driver:
gnat check -Pgnatcheck_example.gpr |
As a result, gnatcheck is called to check all the files from the
project `gnatcheck_example.gpr' using the coding standard defined by
the file `coding_standard'. As the result, the gnatcheck
report file named `gnatcheck.out' will be created in the current
directory, and it will have the following content:
RULE CHECKING REPORT 1. OVERVIEW Date and time of execution: 2009.10.28 14:17 Tool version: GNATCHECK (built with ASIS 2.0.R for GNAT Pro 6.3.0w (20091016)) Command line: gnatcheck -files=.../GNAT-TEMP-000004.TMP -cargs -gnatec=.../GNAT-TEMP-000003.TMP -rules -from=coding_standard Coding standard (applied rules): Abstract_Type_Declarations Anonymous_Arrays EXIT_Statements_With_No_Loop_Name Float_Equality_Checks Local_Packages Compiler style checks: -gnatye Number of coding standard violations: 6 Number of exempted coding standard violations: 1 2. DETECTED RULE VIOLATIONS 2.1. NON-EXEMPTED VIOLATIONS Source files with non-exempted violations pack.ads pack.adb main.adb List of violations grouped by files, and ordered by increasing source location: pack.ads:2:4: declaration of abstract type pack.ads:5:4: declaration of local package pack.ads:10:30: declaration of abstract type pack.ads:11:1: (style) "end Pack" required pack.adb:5:19: use of equality operation for float values pack.adb:6:7: (style) "end Is_Equal" required main.adb:9:26: anonymous array type main.adb:19:10: exit statement with no loop name 2.2. EXEMPTED VIOLATIONS Source files with exempted violations main.adb List of violations grouped by files, and ordered by increasing source location: main.adb:6:18: anonymous array type (this one is fine) 2.3. SOURCE FILES WITH NO VIOLATION No files without violations END OF REPORT |
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |