23. Verifying Properties Using 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 11.15.2 The GNAT Driver and Project Files).

Invoking gnatcheck on the command line has the form:

$ gnatcheck [switches] [-files={arg_list_filename}] [-cargs gcc_switches] [-rules rule_options]

where

• switches specify the general tool options

• Each filename is the name (including the extension) of a source file to process. "Wildcards" are allowed, and the file name may contain path information.

• Each 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.

• gcc_switches is a list of switches for 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.

• rule_options is a list of options for controlling a set of rules to be checked by gnatcheck (see section 23.3 gnatcheck Rule Options).

Either a `filename' or an `arg_list_filename' must be supplied.

23.1 Format of the Report File
23.2 General gnatcheck Switches
23.3 gnatcheck Rule Options
23.4 Adding the Results of Compiler Checks to gnatcheck Output
23.5 Project-Wide Checks
23.6 Predefined Rules

23.1 Format of the Report File

The gnatcheck tool outputs on `stdout' all messages concerning rule violations. It also creates, in the current directory, a text file named `gnatcheck.out' that contains the complete report of the last gnatcheck run. This report contains:

• a list of the Ada source files being checked,
• a list of enabled and disabled rules,
• 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 `stdout'. Section 2 contains messages ordered by rules. Section 3 contains messages ordered by source files.

23.2 General gnatcheck Switches

The following switches control the general gnatcheck behavior

`-a'

Process all units including those with read-only ALI files such as those from GNAT Run-Time library.

`-dd'

Progress indicator mode (for use in GPS)

`-h'

List the predefined and user-defined rules. For more details see 23.6 Predefined Rules.

`-l'

Use full source locations references in the report file. For a construct from a generic instantiation a full source location is a chain from the location of this construct in the generic unit to the place where this unit is instantiated.

`-mnnn'

Maximum number of diagnoses to be sent to Stdout, nnn from o...1000, the default value is 500. Zero means that there is no limitation on the number of diagnostic messages to be printed into Stdout.

`-q'

Quiet mode. All the diagnoses about rule violations are placed in the gnatcheck report file only, without duplicating in `stdout'.

`-s'

Short format of the report file (no version information, no list of applied rules, no list of checked sources is included)

`-s1'

Include the compiler-style section in the report file

`-s2'

Include the section containing diagnoses ordered by rules in the report file

`-s3'

Include the section containing diagnoses ordered by files and then by rules in the report file

`-v'

Verbose mode; gnatcheck generates version information and then a trace of sources being processed.

Note that if any of the options `-s1', `-s2' or `-s3' is specified, then the gnatcheck report file will only contain sections explicitly denoted by these options.

23.3 gnatcheck Rule Options

The following options control the processing performed by gnatcheck.

`+ALL'

Turn all the rule checks ON.

`-ALL'

Turn all the rule checks OFF.

`+Rrule_id[:param]'

Turn on the check for a specified rule with the specified parameter, if any. rule_id must be the identifier of one of the currently implemented rules (use `-h' for the list of implemented rules). Rule identifiers are not case-sensitive. The 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.

`-Rrule_id[:param]'

Turn off the check for a specified rule with the specified parameter, if any.

`-from=rule_option_filename'

Read the rule options from the text file rule_option_filename, referred as "rule file" below.

The default behavior is that all the rule checks are disabled.

A rule file is a text file containing a set of rule options. 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.

A rule file may contain other `-from=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 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'), the processing of rule files is interrupted and a part of their content is ignored.

23.4 Adding the Results of Compiler Checks to 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'

To record restrictions violations (that are performed by the compiler if the pragma Restrictions or Restriction_Warnings are given), use the rule named Restrictions with the same parameters as pragma Restrictions or Restriction_Warnings.

`Style_Checks'

To record compiler style checks(see section 3.2.5 Style Checking), use the rule named Style_Checks. A parameter of this rule can be either All_Checks, which enables all the standard style checks that corresponds to `-gnatyy' GNAT style check option, or a string that has exactly the same structure and semantics as the string_LITERAL parameter of GNAT pragma Style_Checks (for further information about this pragma, see section `Pragma Style_Checks' in GNAT Reference Manual).

`Warnings'

To record compiler warnings (see section 3.2.2 Warning Message Control), use the rule named Warnings with a parameter that is a valid static_string_expression argument of 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.

23.5 Project-Wide Checks

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

23.6 Predefined Rules

The following subsections document the rules implemented in gnatcheck. The subsection title is the same as the rule identifier, which may be used as a parameter of the `+R' or `-R' options.

23.6.1 Abstract_Type_Declarations
23.6.2 Anonymous_Arrays
23.6.3 Anonymous_Subtypes
23.6.4 Blocks
23.6.5 Boolean_Relational_Operators
23.6.6 Controlled_Type_Declarations
23.6.7 Declarations_In_Blocks
23.6.8 Default_Parameters
23.6.9 Discriminated_Records
23.6.10 Enumeration_Ranges_In_CASE_Statements
23.6.11 Exceptions_As_Control_Flow
23.6.12 EXIT_Statements_With_No_Loop_Name
23.6.13 Expanded_Loop_Exit_Names
23.6.14 Explicit_Full_Discrete_Ranges
23.6.15 Float_Equality_Checks
23.6.16 Forbidden_Pragmas
23.6.17 Function_Style_Procedures
23.6.18 Generics_In_Subprograms
23.6.19 GOTO_Statements
23.6.20 Implicit_IN_Mode_Parameters
23.6.21 Implicit_SMALL_For_Fixed_Point_Types
23.6.22 Improperly_Located_Instantiations
23.6.23 Improper_Returns
23.6.24 Library_Level_Subprograms
23.6.25 Local_Packages
23.6.26 Metrics
23.6.27 Misnamed_Identifiers
23.6.28 Multiple_Entries_In_Protected_Definitions
23.6.29 Name_Clashes
23.6.30 Non_Qualified_Aggregates
23.6.31 Non_Short_Circuit_Operators
23.6.32 Non_SPARK_Attributes
23.6.33 Non_Tagged_Derived_Types
23.6.34 Non_Visible_Exceptions
23.6.35 Numeric_Literals
23.6.36 OTHERS_In_Aggregates
23.6.37 OTHERS_In_CASE_Statements
23.6.38 OTHERS_In_Exception_Handlers
23.6.39 Outer_Loop_Exits
23.6.40 Overloaded_Operators
23.6.41 Overly_Nested_Control_Structures
23.6.42 Parameters_Out_Of_Order
23.6.43 Positional_Actuals_For_Defaulted_Generic_Parameters
23.6.44 Positional_Actuals_For_Defaulted_Parameters
23.6.45 Positional_Components
23.6.46 Positional_Generic_Parameters
23.6.47 Positional_Parameters
23.6.48 Predefined_Numeric_Types
23.6.49 Raising_External_Exceptions
23.6.50 Raising_Predefined_Exceptions
23.6.51 Separate_Numeric_Error_Handlers
23.6.52 Slices
23.6.53 Unassigned_OUT_Parameters
23.6.54 Uncommented_BEGIN_In_Package_Bodies
23.6.55 Unconstrained_Array_Returns
23.6.56 Universal_Ranges
23.6.57 Unnamed_Blocks_And_Loops
23.6.58 USE_PACKAGE_Clauses
23.6.59 Volatile_Objects_Without_Address_Clauses

23.6.1 Abstract_Type_Declarations

Flag all declarations of abstract types. For an abstract private type, both the private and full type declarations are flagged.

This rule has no parameters.

23.6.2 Anonymous_Arrays

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

This rule has no parameters.

23.6.3 Anonymous_Subtypes

Flag all uses of anonymous subtypes. A use of an anonymous subtype is any instance of a subtype indication with a constraint, other than one that occurs immediately within a subtype declaration. Any use of a range other than as a constraint used immediately within a subtype declaration is considered as an anonymous subtype.

An effect of this rule is that for loops such as the following are flagged (since 1..N is formally a "range"):

for I in 1 .. N loop ... end loop;

Declaring an explicit subtype solves the problem:

subtype S is Integer range 1..N; ... for I in S loop ... end loop;

This rule has no parameters.

23.6.4 Blocks

Flag each block statement.

This rule has no parameters.

23.6.5 Boolean_Relational_Operators

Flag each call to a predefined relational operator ("<", ">", "<=", ">=", "=" and "/=") for the predefined Boolean type. (This rule is useful in enforcing the SPARK language restrictions.)

Calls to predefined relational operators of any type derived from Standard.Boolean are not detected. Calls to user-defined functions with these designators, and uses of operators that are renamings of the predefined relational operators for Standard.Boolean, are likewise not detected.

This rule has no parameters.

23.6.6 Controlled_Type_Declarations

Flag all declarations of controlled types. A declaration of a private type is flagged if its full declaration declares a controlled type. A declaration of a derived type is flagged if its ancestor type is controlled. Subtype declarations are not checked. A declaration of a type that itself is not a descendant of a type declared in Ada.Finalization but has a controlled component is not checked.

This rule has no parameters.

23.6.7 Declarations_In_Blocks

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

This rule has no parameters.

23.6.8 Default_Parameters

Flag all default expressions for subprogram parameters. Parameter declarations of formal and generic subprograms are also checked.

This rule has no parameters.

23.6.9 Discriminated_Records

Flag all declarations of record types with discriminants. Only the declarations of record and record extension types are checked. Incomplete, formal, private, derived and private extension type declarations are not checked. Task and protected type declarations also are not checked.

This rule has no parameters.

23.6.10 Enumeration_Ranges_In_CASE_Statements

Flag each use of a range of enumeration literals as a choice in a case statement. All forms for specifying a range (explicit ranges such as A .. B, subtype marks and 'Range attributes) are flagged. An enumeration range is flagged even if contains exactly one enumeration value or no values at all. A type derived from an enumeration type is considered as an enumeration type.

This rule helps prevent maintenance problems arising from adding an enumeration value to a type and having it implicitly handled by an existing case statement with an enumeration range that includes the new literal.

This rule has no parameters.

23.6.11 Exceptions_As_Control_Flow

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

The rule has no parameters.

23.6.12 EXIT_Statements_With_No_Loop_Name

Flag each exit statement that does not specify the name of the loop being exited.

The rule has no parameters.

23.6.13 Expanded_Loop_Exit_Names

Flag all expanded loop names in exit statements.

This rule has no parameters.

23.6.14 Explicit_Full_Discrete_Ranges

Flag each discrete range that has the form A'First .. A'Last.

This rule has no parameters.

23.6.15 Float_Equality_Checks

Flag all calls to the predefined equality operations for floating-point types. Both "=" and "/=" operations are checked. User-defined equality operations are not flagged, nor are "=" and "/=" operations for fixed-point types.

This rule has no parameters.

23.6.16 Forbidden_Pragmas

Flag each use of the specified pragmas. The pragmas to be detected are named in the rule's parameters.

This rule has the following parameters:

• For the `+R' option

  Pragma_Name

  Adds the specified pragma to the set of pragmas to be checked and sets the checks for all the specified pragmas ON. Pragma_Name is treated as a name of a pragma. If it does not correspond to any pragma name defined in the Ada standard or to the name of a GNAT-specific pragma defined in section `Implementation Defined Pragmas' in GNAT Reference Manual, it is treated as the name of unknown pragma.

  GNAT

  All the GNAT-specific pragmas are detected; this sets the checks for all the specified pragmas ON.

  ALL

  All pragmas are detected; this sets the rule ON.

• For the `-R' option

  Pragma_Name

  Removes the specified pragma from the set of pragmas to be checked without affecting checks for other pragmas. Pragma_Name is treated as a name of a pragma. If it does not correspond to any pragma defined in the Ada standard or to any name defined in section `Implementation Defined Pragmas' in GNAT Reference Manual, this option is treated as turning OFF detection of all unknown pragmas.

  GNAT

  Turn OFF detection of all GNAT-specific pragmas

  ALL

  Clear the list of the pragmas to be detected and turn the rule OFF.

Parameters are not case sensitive. If Pragma_Name does not have the syntax of an Ada identifier and therefore can not be considered as a pragma name, a diagnostic message is generated and the corresponding parameter is ignored.

When more then one parameter is given in the same rule option, the parameters must be separated by a comma.

If more then one option for this rule is specified for the gnatcheck call, a new option overrides the previous one(s).

The `+R' option with no parameters turns the rule ON with the set of pragmas to be detected defined by the previous rule options. (By default this set is empty, so if the only option specified for the rule is `+RForbidden_Pragmas' (with no parameter), then the rule is enabled, but it does not detect anything). The `-R' option with no parameter turns the rule OFF, but it does not affect the set of pragmas to be detected.

23.6.17 Function_Style_Procedures

Flag each procedure that can be rewritten as a function. A procedure can be converted into a function if it has exactly one parameter of mode out and no parameters of mode in out. Procedure declarations, formal procedure declarations, and generic procedure declarations are always checked. Procedure bodies and body stubs are flagged only if they do not have corresponding separate declarations. Procedure renamings and procedure instantiations are not flagged.

If a procedure can be rewritten as a function, but its out parameter is of a limited type, it is not flagged.

Protected procedures are not flagged. Null procedures also are not flagged.

This rule has no parameters.

23.6.18 Generics_In_Subprograms

Flag each declaration of a generic unit in a subprogram. Generic declarations in the bodies of generic subprograms are also flagged. A generic unit nested in another generic unit is not flagged. If a generic unit is declared in a local package that is declared in a subprogram body, the generic unit is flagged.

This rule has no parameters.

23.6.19 GOTO_Statements

Flag each occurrence of a goto statement.

This rule has no parameters.

23.6.20 Implicit_IN_Mode_Parameters

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

This rule has no parameters.

23.6.21 Implicit_SMALL_For_Fixed_Point_Types

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

This rule has no parameters.

23.6.22 Improperly_Located_Instantiations

Flag all generic instantiations in library-level package specs (including library generic packages) and in all subprogram bodies.

Instantiations in task and entry bodies are not flagged. Instantiations in the bodies of protected subprograms are flagged.

This rule has no parameters.

23.6.23 Improper_Returns

Flag each explicit return statement in procedures, and multiple return statements in functions. Diagnostic messages are generated for all return statements in a procedure (thus each procedure must be written so that it returns implicitly at the end of its statement part), and for all return statements in a function after the first one. This rule supports the stylistic convention that each subprogram should have no more than one point of normal return.

This rule has no parameters.

23.6.24 Library_Level_Subprograms

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

This rule has no parameters.

23.6.25 Local_Packages

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

This rule has no parameters.

23.6.26 Metrics

There is a set of checks based on computing a metric value and comparing the result with the specified upper (or lower, depending on a specific metric) value specified for a given metric. A construct is flagged if a given metric is applicable (can be computed) for it and the computed value is greater then (lover then) the specified upper (lower) bound.

The name of any metric-based rule consists of the prefix Metrics_ followed by the name of the corresponding metric (see the table below). For `+R' option, each metric-based rule has a numeric parameter specifying the bound (integer or real, depending on a metric), `-R' option for metric rules does not have a parameter.

The following table shows the metric names for that the corresponding metrics-based checks are supported by gnatcheck, including the constraint that must be satisfied by the bound that is specified for the check and what bound - upper (U) or lower (L) - should be specified.

Check Name	Description	Bounds Value
Essential_Complexity	Essential complexity	Positive integer (U)
Cyclomatic_Complexity	Cyclomatic complexity	Positive integer (U)
LSLOC	Logical Source Lines of Code	Positive integer (U)

The meaning and the computed values for all these metrics are exactly the same as for the corresponding metrics in gnatmetric.

Example: the rule

+RMetrics_Cyclomatic_Complexity : 7

means that all bodies with cyclomatic complexity exceeding 7 will be flagged.

To turn OFF the check for cyclomatic complexity metric, use the following option:

-RMetrics_Cyclomatic_Complexity

23.6.27 Misnamed_Identifiers

Flag the declaration of each identifier that does not have a suffix corresponding to the kind of entity being declared. The following declarations are checked:

• type declarations

• constant declarations (but not number declarations)

• package renaming declarations (but not generic package renaming declarations)

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

• type-defining names end with _T, unless the type is an access type, in which case the suffix must be _A
• constant names end with _C
• names defining package renamings end with _R

For a private or incomplete type declaration the following checks are made for the defining name suffix:

• 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.

• 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.

For a deferred constant, the defining name in the corresponding full constant declaration is not checked.

Defining names of formal types are not checked.

The rule may have the following parameters:

• For the `+R' option:

  Default

  Sets the default listed above for all the names to be checked.

  Type_Suffix=string

  Specifies the suffix for a type name.

  Access_Suffix=string

  Specifies the suffix for an access type name. If this parameter is set, it overrides for access types the suffix set by the Type_Suffix parameter.

  Constant_Suffix=string

  Specifies the suffix for a constant name.

  Renaming_Suffix=string

  Specifies the suffix for a package renaming name.

• For the `-R' option:

  All_Suffixes

  Remove all the suffixes specified for the identifier suffix checks, whether by default or as specified by other rule parameters. All the checks for this rule are disabled as a result.

  Type_Suffix

  Removes the suffix specified for types. This disables checks for types but does not disable any other checks for this rule (including the check for access type names if Access_Suffix is set).

  Access_Suffix

  Removes the suffix specified for access types. This disables checks for access type names but does not disable any other checks for this rule. If Type_Suffix is set, access type names are checked as ordinary type names.

  Constant_Suffix

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

  Renaming_Suffix

  Removes the suffix specified for package renamings. This disables checks for package renamings but does not disable any other checks for this rule.

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

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

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

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

The string value must be a valid suffix for an Ada identifier (after trimming all the leading and trailing space characters, if any). Parameters are not case sensitive, except the string part.

If any error is detected in a rule parameter, the parameter is ignored. In such a case the options that are set for the rule are not specified.

23.6.28 Multiple_Entries_In_Protected_Definitions

Flag each protected definition (i.e., each protected object/type declaration) that defines more than one entry. Diagnostic messages are generated for all the entry declarations except the first one. An entry family is counted as one entry. Entries from the private part of the protected definition are also checked.

This rule has no parameters.

23.6.29 Name_Clashes

Check that certain names are not used as defining identifiers. To activate this rule, you need to supply a reference to the dictionary file(s) as a rule parameter(s) (more then one dictionary file can be specified). If no dictionary file is set, this rule will not cause anything to be flagged. Only defining occurrences, not references, are checked. The check is not case-sensitive.

This rule is enabled by default, but without setting any corresponding dictionary file(s); thus the default effect is to do no checks.

A dictionary file is a plain text file. The maximum line length for this file is 1024 characters. If the line is longer then this limit, extra characters are ignored.

Each line can be either an empty line, a comment line, or a line containing a list of identifiers separated by space or HT characters. A comment is an Ada-style comment (from -- to end-of-line). Identifiers must follow the Ada syntax for identifiers. A line containing one or more identifiers may end with a comment.

23.6.30 Non_Qualified_Aggregates

Flag each non-qualified aggregate. A non-qualified aggregate is an aggregate that is not the expression of a qualified expression. A string literal is not considered an aggregate, but an array aggregate of a string type is considered as a normal aggregate. Aggregates of anonymous array types are not flagged.

This rule has no parameters.

23.6.31 Non_Short_Circuit_Operators

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

This rule has no parameters.

23.6.32 Non_SPARK_Attributes

The SPARK language defines the following subset of Ada 95 attribute designators as those that can be used in SPARK programs. The use of any other attribute is flagged.

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

This rule has no parameters.

23.6.33 Non_Tagged_Derived_Types

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

This rule has no parameters.

23.6.34 Non_Visible_Exceptions

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

• An exception declaration in a subprogram body, task body or block statement is flagged if the body or statement does not contain a handler for that exception or a handler with an others choice.

• A raise statement in an exception handler of a subprogram body, task body or block statement is flagged if it (re)raises a locally declared exception. This may occur under the following circumstances:
  • it explicitly raises a locally declared exception, or
  • it does not specify an exception name (i.e., it is simply raise;) and the enclosing handler contains a locally declared exception in its exception choices.

Renamings of local exceptions are not flagged.

This rule has no parameters.

23.6.35 Numeric_Literals

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

• a literal occurring in the initialization expression for a constant declaration or a named number declaration, or

• an integer literal that is less than or equal to a value specified by the `N' rule parameter.

This rule may have the following parameters for the `+R' option:

N

N is an integer literal used as the maximal value that is not flagged (i.e., integer literals not exceeding this value are allowed)

ALL

All integer literals are flagged

If no parameters are set, the maximum unflagged value is 1.

The last specified check limit (or the fact that there is no limit at all) is used when multiple `+R' options appear.

The `-R' option for this rule has no parameters. It disables the rule but retains the last specified maximum unflagged value. If the `+R' option subsequently appears, this value is used as the threshold for the check.

23.6.36 OTHERS_In_Aggregates

Flag each use of an others choice in extension aggregates. In record and array aggregates, an others choice is flagged unless it is used to refer to all components, or to all but one component.

If, in case of a named array aggregate, there are two associations, one with an others choice and another with a discrete range, the others choice is flagged even if the discrete range specifies exactly one component; for example, (1..1 => 0, others => 1).

This rule has no parameters.

23.6.37 OTHERS_In_CASE_Statements

Flag any use of an others choice in a case statement.

This rule has no parameters.

23.6.38 OTHERS_In_Exception_Handlers

Flag any use of an others choice in an exception handler.

This rule has no parameters.

23.6.39 Outer_Loop_Exits

Flag each exit statement containing a loop name that is not the name of the immediately enclosing loop statement.

This rule has no parameters.

23.6.40 Overloaded_Operators

Flag each function declaration that overloads an operator symbol. A function body is checked only if the body does not have a separate spec. Formal functions are also checked. For a renaming declaration, only renaming-as-declaration is checked

This rule has no parameters.

23.6.41 Overly_Nested_Control_Structures

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

The control structures checked are the following:

• if statement
• case statement
• loop statement
• Selective accept statement
• Timed entry call statement
• Conditional entry call
• Asynchronous select statement

The rule has the following parameter for the `+R' option:

N

Positive integer specifying the maximal control structure nesting level that is not flagged

If the parameter for the `+R' option is not specified or if it is not a positive integer, `+R' option is ignored.

If more then one option is specified for the gnatcheck call, the later option and new parameter override the previous one(s).

23.6.42 Parameters_Out_Of_Order

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

• in and access parameters first, then in out parameters, and then out parameters;

• for in mode, parameters with default initialization expressions occur last

Only the first violation of the described order is flagged.

The following constructs are checked:

• subprogram declarations (including null procedures);
• generic subprogram declarations;
• formal subprogram declarations;
• entry declarations;
• subprogram bodies and subprogram body stubs that do not have separate specifications

Subprogram renamings are not checked.

This rule has no parameters.

23.6.43 Positional_Actuals_For_Defaulted_Generic_Parameters

Flag each generic actual parameter corresponding to a generic formal parameter with a default initialization, if positional notation is used.

This rule has no parameters.

23.6.44 Positional_Actuals_For_Defaulted_Parameters

Flag each actual parameter to a subprogram or entry call where the corresponding formal parameter has a default expression, if positional notation is used.

This rule has no parameters.

23.6.45 Positional_Components

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

This rule has no parameters.

23.6.46 Positional_Generic_Parameters

Flag each instantiation using positional parameter notation.

This rule has no parameters.

23.6.47 Positional_Parameters

Flag each subprogram or entry call using positional parameter notation, except for the following:

• Invocations of prefix or infix operators are not flagged
• If the called subprogram or entry has only one formal parameter, the call is not flagged;
• If a subprogram call uses the Object.Operation notation, then
  • the first parameter (that is, Object) is not flagged;
  • if the called subprogram has only two parameters, the second parameter of the call is not flagged;

This rule has no parameters.

23.6.48 Predefined_Numeric_Types

Flag each explicit use of the name of any numeric type or subtype defined in package Standard.

The rationale for this rule is to detect when the program may depend on platform-specific characteristics of the implementation of the predefined numeric types. Note that this rule is over-pessimistic; for example, a program that uses String indexing likely needs a variable of type Integer. Another example is the flagging of predefined numeric types with explicit constraints:

subtype My_Integer is Integer range Left .. Right; Vy_Var : My_Integer;

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

This rule has no parameters.

23.6.49 Raising_External_Exceptions

Flag any raise statement, in a program unit declared in a library package or in a generic library package, for an exception that is neither a predefined exception nor an exception that is also declared (or renamed) in the visible part of the package.

This rule has no parameters.

23.6.50 Raising_Predefined_Exceptions

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

This rule has no parameters.

23.6.51 Separate_Numeric_Error_Handlers

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

This rule has no parameters.

23.6.52 Slices

Flag all uses of array slicing

This rule has no parameters.

23.6.53 Unassigned_OUT_Parameters

Flags procedures' out parameters that are not assigned, and identifies the contexts in which the assignments are missing.

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

An out parameter is flagged in an exception handler in the exception part of the procedure body's handled sequence of statements if the handler contains no assignment to the parameter.

Bodies of generic procedures are also considered.

The following are treated as assignments to an out parameter:

• an assignment statement, with the parameter or some component as the target;

• passing the parameter (or one of its components) as an out or in out parameter.

This rule does not have any parameters.

23.6.54 Uncommented_BEGIN_In_Package_Bodies

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

If the begin keyword is placed on the same line as the last declaration or the first statement, it is flagged independently of whether the line contains a trailing comment. The diagnostic message is attached to the line containing the first statement.

This rule has no parameters.

23.6.55 Unconstrained_Array_Returns

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 not checked.

This rule has no parameters.