10. Predefined Rules

The description of the rules currently implemented in gnatcheck is given in this chapter. The rule identifier is used as a parameter of gnatcheck‘s +R or -R switches.

Be aware that most of these rules apply to specialized coding requirements developed by individual users and may well not make sense in other environments. In particular, there are many rules that conflict with one another. Proper usage of gnatcheck involves selecting the rules you wish to apply by looking at your independently developed coding standards and finding the corresponding gnatcheck rules.

If not otherwise specified, a rule does not do any check for the results of generic instantiations.

10.2. Feature Usage Rules

The rules in this section can be used to enforce specific usage patterns for a variety of language features.

10.2.1. Abort_Statements

Flag abort statements.

This rule has no parameters.

Example

if Flag then
   abort T;    --  FLAG
end if;

10.2.2. Abstract_Type_Declarations

Flag all declarations of abstract types, including generic formal types. For an abstract private type, the full type declarations is flagged only if it is itself declared as abstract. Interface types are not flagged.

This rule has no parameters.

Example

package Foo is
   type Figure is abstract tagged private;              --  FLAG
   procedure Move (X : in out Figure) is abstract;
private
   type Figure is abstract tagged null record;          --  FLAG
end Foo;

10.2.3. Anonymous_Subtypes

Flag all uses of anonymous subtypes except for the following:

  • when the subtype indication depends on a discriminant, this includes the cases of a record component definitions when a component depends on a discriminant, and using the discriminant of the derived type to constraint the parent type;
  • when a self-referenced data structure is defined, and a discriminant is constrained by the reference to the current instance of a type;

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.

The rule does not flag ranges in the component clauses from a record representation clause, because the language rules do not allow to use subtype names there.

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   --  FLAG
   ...
end loop;

Declaring an explicit subtype solves the problem:

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

This rule has no parameters.

10.2.4. Blocks

Flag each block statement.

This rule has no parameters.

Example

if I /= J then
   declare             --  FLAG
      Tmp : Integer;
   begin
      TMP := I;
      I   := J;
      J   := Tmp;
   end;
end if;

10.2.5. Complex_Inlined_Subprograms

Flag a subprogram (or generic subprogram, or instantiation of a subprogram) if pragma Inline is applied to it and at least one of the following conditions is met:

  • it contains at least one complex declaration such as a subprogram body, package, task, protected declaration, or a generic instantiation (except instantiation of Ada.Unchecked_Conversion);
  • it contains at least one complex statement such as a loop, a case or an if statement;
  • the number of statements exceeds a value specified by the N rule parameter;

Subprogram renamings are also considered.

This rule has the following (mandatory) parameter for the +R option:

N
Positive integer specifying the maximum allowed total number of statements in the subprogram body.

Example

procedure Swap (I, J : in out Integer) with Inline => True;

procedure Swap (I, J : in out Integer) is   --  FLAG
begin

   if I /= J then
      declare
         Tmp : Integer;
      begin
         TMP := I;
         I   := J;
         J   := Tmp;
      end;
   end if;

end Swap;

10.2.6. Conditional_Expressions

Flag use of conditional expression.

This rule has the following (optional) parameters for the +R option:

Except_Assertions
Do not flag a conditional expression if it is a subcomponent of the following constructs:

argument of the following pragmas

Language-defined

  • Assert

GNAT-specific

  • Assert_And_Cut
  • Assume
  • Contract_Cases
  • Debug
  • Invariant
  • Loop_Invariant
  • Loop_Variant
  • Postcondition
  • Precondition
  • Predicate
  • Refined_Post

definition of the following aspects

Language-defined

  • Static_Predicate
  • Dynamic_Predicate
  • Pre
  • Pre'Class
  • Post
  • Post'Class
  • Type_Invariant
  • Type_Invariant'Class

GNAT-specific

  • Contract_Cases
  • Invariant
  • Invariant'Class
  • Predicate
  • Refined_Post

Example

Var1 : Integer := (if I > J then 1 else 0);  --  FLAG
Var2 : Integer := I + J;

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

Example

with Ada.Finalization;
package Foo is
   type Resource is new Ada.Finalization.Controlled with private;  --  FLAG

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

Example

if I /= J then
   declare                       --  FLAG
      Tmp : Integer;
   begin
      TMP := I;
      I   := J;
      J   := Tmp;
   end;
end if;

10.2.9. Deeply_Nested_Inlining

Flag a subprogram (or generic subprogram) if pragma Inline has been applied to it, and it calls another subprogram to which pragma Inline applies, resulting in potential nested inlining, with a nesting depth exceeding the value specified by the N rule parameter.

This rule requires the global analysis of all the compilation units that are gnatcheck arguments; such analysis may affect the tool’s performance. If gnatcheck generates warnings saying that “body is not analyzed for ...”, this means that such an analysis is incomplete, this may result in rule false negatives.

This rule has the following (mandatory) parameter for the +R option:

N
Positive integer specifying the maximum level of nested calls to subprograms to which pragma Inline has been applied.

Example

procedure P1 (I : in out integer) with Inline => True;   --  FLAG
procedure P2 (I : in out integer) with Inline => True;
procedure P3 (I : in out integer) with Inline => True;
procedure P4 (I : in out integer) with Inline => True;

procedure P1 (I : in out integer) is
begin
   I := I + 1;
   P2 (I);
end;

procedure P2 (I : in out integer) is
begin
   I := I + 1;
   P3 (I);
end;

procedure P3 (I : in out integer) is
begin
   I := I + 1;
   P4 (I);
end;

procedure P4 (I : in out integer) is
begin
   I := I + 1;
end;

10.2.10. Default_Parameters

Flag all default expressions in parameters specifications. All parameter specifications are checked: in subprograms (including formal, generic and protected subprograms) and in task and protected entries (including accept statements and entry bodies).

This rule has no parameters.

Example

procedure P (I : in out Integer; J : Integer := 0);   --  FLAG
procedure Q (I : in out Integer; J : Integer);

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

Example

type Idx is range 1 .. 100;
type Arr is array (Idx range <>) of Integer;
subtype Arr_10 is Arr (1 .. 10);

type Rec_1 (D : Idx) is record        --  FLAG
   A : Arr (1 .. D);
end record;

type Rec_2 (D : Idx) is record        --  FLAG
   B : Boolean;
end record;

type Rec_3 is record
   B : Boolean;
end record;

10.2.12. Explicit_Full_Discrete_Ranges

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

This rule has no parameters.

Example

   subtype Idx is Integer range 1 .. 100;
begin
   for J in Idx'First .. Idx'Last loop   --  FLAG
      K := K + J;
   end loop;

   for J in Idx loop
      L := L + J;
   end loop;

10.2.13. Expression_Functions

Flag each expression function declared in a package specification (including specification of local packages and generic package specifications).

This rule has no parameters.

Example

package Foo is

   function F (I : Integer) return Integer is   --  FLAG
     (if I > 0 then I - 1 else I + 1);

10.2.14. Fixed_Equality_Checks

Flag all explicit calls to the predefined equality operations for fixed-point types. Both ‘=‘ and ‘/=‘ operations are checked. User-defined equality operations are not flagged, nor are uses of operators that are renamings of the predefined equality operations. Also, the ‘=‘ and ‘/=‘ operations for floating-point types are not flagged.

This rule has no parameters.

Example

package Pack is
     type Speed is delta 0.01 range 0.0 .. 10_000.0;
     function Get_Speed return Speed;
end Pack;

with Pack; use Pack;
procedure Process is
     Speed1 : Speed := Get_Speed;
     Speed2 : Speed := Get_Speed;

     Flag : Boolean := Speed1 = Speed2;     --  FLAG

10.2.15. Float_Equality_Checks

Flag all explicit calls to the predefined equality operations for floating-point types and private types whose completions are floating-point types. Both ‘=‘ and ‘/=‘ operations are checked. User-defined equality operations are not flagged, nor are uses of operators that are renamings of the predefined equality operations. Also, the ‘=‘ and ‘/=‘ operations for fixed-point types are not flagged.

This rule has no parameters.

Example

package Pack is
     type Speed is digits 0.01 range 0.0 .. 10_000.0;
     function Get_Speed return Speed;
end Pack;

with Pack; use Pack;
procedure Process is
     Speed1 : Speed := Get_Speed;
     Speed2 : Speed := Get_Speed;

     Flag : Boolean := Speed1 = Speed2;     --  FLAG

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

Example

procedure Cannot_be_a_function (A, B : out Boolean);
procedure Can_be_a_function (A : out Boolean);           --  FLAG

10.2.17. Generic_IN_OUT_Objects

Flag declarations of generic formal objects of mode IN OUT.

This rule has no parameters.

Example

generic
   I :        Integer;
   J : in     Integer;
   K : in out Integer;             --  FLAG
package Pack_G is

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

Example

procedure Proc is

   generic                                --  FLAG
      type FT is range <>;
   function F_G (I : FT) return FT;

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

Example

procedure Proc1 (I :    Integer);          --  FLAG
procedure Proc2 (I : in Integer);
procedure Proc3 (I :    access Integer);

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

Example

with Ada.Text_IO; use Ada.Text_IO;
procedure Proc is
   package My_Int_IO is new Integer_IO (Integer);   --  FLAG

10.2.21. Library_Level_Subprograms

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

This rule has no parameters.

with Ada.Text_IO; use Ada.Text_IO;
procedure Proc is                         --  FLAG

10.2.22. Membership_Tests

Flag use of membership test expression.

This rule has the following (optional) parameters for the +R option:

Multi_Alternative_Only
Flag only those membership test expressions that have more than one membership choice in the membership choice list.
Float_Types_Only
Flag only those membership test expressions that checks objects of floating point type and private types whose completions are floating-point types.
Except_Assertions
Do not flag a membership test expression if it is a subcomponent of the following constructs:

argument of the following pragmas

Language-defined

  • Assert

GNAT-specific

  • Assert_And_Cut
  • Assume
  • Contract_Cases
  • Debug
  • Invariant
  • Loop_Invariant
  • Loop_Variant
  • Postcondition
  • Precondition
  • Predicate
  • Refined_Post

definition of the following aspects

Language-defined

  • Static_Predicate
  • Dynamic_Predicate
  • Pre
  • Pre'Class
  • Post
  • Post'Class
  • Type_Invariant
  • Type_Invariant'Class

GNAT-specific

  • Contract_Cases
  • Invariant
  • Invariant'Class
  • Predicate
  • Refined_Post

These three parameters are independent on each other.

Example

procedure Proc (S : in out Speed) is
begin
   if S in Low .. High then      --  FLAG

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

Example

type Arr is array (1 .. 10) of Integer;

Var1 : Arr := (1 => 10, 2 => 20, others => 30);             --  FLAG
Var2 : array (1 .. 10) of Integer := (1 => 10, 2 => 20, others => 30);

10.2.24. Number_Declarations

Number declarations are flagged.

This rule has no parameters.

Example

Num1 : constant := 13;                 --  FLAG
Num2 : constant := 1.3;                --  FLAG

Const1 : constant Integer := 13;
Const2 : constant Float := 1.3;

10.2.25. Numeric_Indexing

Flag numeric literals, including those preceded by a predefined unary minus, if they are used as index expressions in array components. Literals that are subcomponents of index expressions are not flagged (other than the aforementioned case of unary minus).

This rule has no parameters.

Example

procedure Proc is
   type Arr is array (1 .. 10) of Integer;
   Var : Arr;
begin
   Var (1) := 10;       --  FLAG

10.2.26. Numeric_Literals

Flag each use of a numeric literal except for the following:

  • a literal occurring in the initialization expression for a constant declaration or a named number declaration, or
  • a literal occurring in an aspect definition or in an aspect clause, or
  • an integer literal that is less than or equal to a value specified by the N rule parameter.
  • a literal occurring in a declaration in case the Statements_Only rule parameter is given

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
Statements_Only
Numeric literals are flagged only when used in statements

If no parameters are set, the maximum unflagged value is 1, and the check for literals is not limited by statements only.

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 and restores its default operation mode. If the +R option subsequently appears, will be 1, and the check will not be limited by statements only.

Example

C1 : constant Integer := 10;
V1 :          Integer := C1;
V2 :          Integer := 20;      --  FLAG

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

Example

procedure Proc1 (I : in out Integer; B : Boolean) is    --  FLAG

10.2.28. Predicate_Testing

Flag a subtype mark if it denotes a subtype defined with (static or dynamic) subtype predicate and is used as a membership choice in a membership test expression.

Flags ‘Valid attribute reference if the nominal subtype of the attribute prefix has (static or dynamic) subtype predicate.

This rule has the following (optional) parameters for the +R option:

Except_Assertions
Do not flag a construct described above if it is a subcomponent of the following constructs:

argument of the following pragmas

Language-defined

  • Assert

GNAT-specific

  • Assert_And_Cut
  • Assume
  • Contract_Cases
  • Debug
  • Invariant
  • Loop_Invariant
  • Loop_Variant
  • Postcondition
  • Precondition
  • Predicate
  • Refined_Post

definition of the following aspects

Language-defined

  • Static_Predicate
  • Dynamic_Predicate
  • Pre
  • Pre'Class
  • Post
  • Post'Class
  • Type_Invariant
  • Type_Invariant'Class

GNAT-specific

  • Contract_Cases
  • Invariant
  • Invariant'Class
  • Predicate
  • Refined_Post

Example

with Support; use Support;
package Pack is
   subtype Even is Integer with Dynamic_Predicate => Even mod 2 = 0;

   subtype Small_Even is Even range -100 .. 100;

   B1 : Boolean := Ident (101) in Small_Even;      --  FLAG

10.2.29. Relative_Delay_Statements

Relative delay statements are flagged. Delay until statements are not flagged.

This rule has no parameters.

Example

if I > 0 then
   delay until Current_Time + Big_Delay;
else
   delay Small_Delay;                      --  FLAG
end if;

10.2.30. Renamings

Flag renaming declarations.

This rule has no parameters.

Example

I : Integer;
J : Integer renames I;     --  FLAG

10.2.31. Representation_Specifications

Flag each record representation clause, enumeration representation clause and representation attribute clause. Flag each aspect definition that defines a representation aspect. Also flag any pragma that is classified by the Ada Standard as a representation pragma, and the definition of the corresponding aspects.

The rule has an optional parameter for +R option:

Record_Types_Only
Only the representation items that are applied to record types are flagged.

Example

type State         is (A,M,W,P);
type Mode          is (Fix, Dec, Exp, Signif);

type Byte_Mask     is array (0..7)  of Boolean
  with Component_Size => 1;                                --  FLAG

type State_Mask    is array (State) of Boolean
  with Component_Size => 1;                                --  FLAG

type Mode_Mask     is array (Mode)  of Boolean;
for Mode_Mask'Component_Size use 1;                        --  FLAG

10.2.32. Quantified_Expressions

Flag use of quantified expression.

This rule has the following (optional) parameters for the +R option:

Except_Assertions
Do not flag a conditional expression if it is a subcomponent of the following constructs:

argument of the following pragmas

Language-defined

  • Assert

GNAT-specific

  • Assert_And_Cut
  • Assume
  • Contract_Cases
  • Debug
  • Invariant
  • Loop_Invariant
  • Loop_Variant
  • Postcondition
  • Precondition
  • Predicate
  • Refined_Post

definition of the following aspects

Language-defined

  • Static_Predicate
  • Dynamic_Predicate
  • Pre
  • Pre'Class
  • Post
  • Post'Class
  • Type_Invariant
  • Type_Invariant'Class

GNAT-specific

  • Contract_Cases
  • Invariant
  • Invariant'Class
  • Predicate
  • Refined_Post

Example

subtype Ind is Integer range 1 .. 10;
type Matrix is array (Ind, Ind) of Integer;

function Check_Matrix (M : Matrix) return Boolean is
  (for some I in Ind =>                               --  FLAG
     (for all J in Ind => M (I, J) = 0));             --  FLAG

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

Example

begin
   raise Constraint_Error;    --  FLAG

10.2.34. Subprogram_Access

Flag all constructs that belong to access_to_subprogram_definition syntax category, and all access definitions that define access to subprogram.

This rule has no parameters.

Example

type Proc_A is access procedure ( I : Integer);       --  FLAG

procedure Proc
  (I       : Integer;
   Process : access procedure (J : in out Integer));  --  FLAG

10.2.35. Too_Many_Dependencies

Flag a library item or a subunit that immediately depends on more than N library units (N is a rule parameter). In case of a dependency on child units, implicit or explicit dependencies on all their parents are not counted.

This rule has the following (mandatory) parameters for the +R option:

N
Positive integer specifying the maximal number of dependencies when the library item or subunit is not flagged.

Example

--  if rule parameter is 5 or smaller:
with Pack1;
with Pack2;
with Pack3;
with Pack4;
with Pack5;
with Pack6;
procedure Main is               --  FLAG

10.2.36. Unassigned_OUT_Parameters

Flag procedures’ out parameters that are not assigned.

An out parameter is flagged if the sequence of statements of the procedure body (before the procedure body’s exception part, if any) contains no assignment to the parameter.

An out parameter is flagged in an exception handler in the exception part of the procedure body, if the exception handler contains neither an assignment to the parameter nor a raise statement.

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, except for the case when it is passed to the call of an attribute subprogram.

This rule has no parameters.

Warning

This rule only detects a trivial case of an unassigned variable and doesn’t provide a guarantee that there is no uninitialized access. The rule does not check function parameters (starting from Ada 2012 functions can have out parameters). It is not a replacement for rigorous check for uninitialized access provided by advanced static analysis tools.

Example

procedure Proc                --  FLAG
  (I    : Integer;
   Out1 : out Integer;
   Out2 : out Integer)
is
begin
   Out1 := I + 1;
end Proc;

10.2.37. 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 flagged. Function calls and function renamings are not flagged.

Generic function declarations, and function declarations in generic packages, are not flagged. Instead, this rule flags the results of generic instantiations (that is, expanded specification and expanded body corresponding to an instantiation).

This rule has the following (optional) parameters for the +R option:

Except_String
Do not flag functions that return the predefined String type or a type derived from it, directly or indirectly.

Example

type Arr is array (Integer range <>) of Integer;
subtype Arr_S is Arr (1 .. 10);

function F1 (I : Integer) return Arr;      --  FLAG
function F2 (I : Integer) return Arr_S;

10.2.38. Unconstrained_Arrays

Unconstrained array definitions are flagged.

This rule has no parameters.

Example

type Idx is range -100 .. 100;

type U_Arr is array (Idx range <>) of Integer;      --  FLAG
type C_Arr is array (Idx) of Integer;

10.4. SPARK Ada Rules

The rules in this section can be used to enforce compliance with the Ada subset allowed by the SPARK tools.

10.4.1. Annotated_Comments

Flags comments that are used as annotations or as special sentinels/markers. Such comments have the following structure

--<special_character> <comment_marker>

where

<special_character>
character (such as ‘#’, ‘$’, ‘|’ etc.) indicating that the comment is used for a specific purpose
<comment_marker>
a word identifying the annotation or special usage (word here is any sequence of characters except white space)

There may be any amount of white space (including none at all) between <special_character> and <comment_marker>, but no white space is permitted between '--' and <special_character>. (A white space here is either a space character or horizontal tabulation)

<comment_marker> must not contain any white space.

<comment_marker> may be empty, in which case the rule flags each comment that starts with --<special_character> and that does not contain any other character except white space

The rule has the following (mandatory) parameter for the +R option:

S
String with the following interpretation: the first character is the special comment character, and the rest is the comment marker. S must not contain white space.

The -R option erases all definitions of special comment annotations specified by the previous +R options.

The rule is case-sensitive.

Example:

The rule

+RAnnotated_Comments:#hide

will flag the following comment lines

--#hide
--# hide
--#           hide

   I := I + 1; --# hide

But the line

-- # hide

will not be flagged, because of the space between ‘–’ and ‘#’.

The line

--#Hide

will not be flagged, because the string parameter is case sensitive.

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

Example

   procedure Proc (Flag_1 : Boolean; Flag_2 : Boolean; I : in out Integer) is
   begin
      if Flag_1 >= Flag_2 then     --  FLAG

10.4.3. Expanded_Loop_Exit_Names

Flag all expanded loop names in exit statements.

This rule has no parameters.

Example

procedure Proc (S : in out String) is
begin
   Search : for J in S'Range loop
      if S (J) = ' ' then
         S (J) := '_';
         exit Proc.Search;            --  FLAG
      end if;
   end loop Search;
end Proc;

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

Example

type Integer_A is access all Integer;

Var : aliased Integer := 1;
Var_A : Integer_A := Var'Access;  --  FLAG

10.4.5. Non_Tagged_Derived_Types

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

This rule has no parameters.

Example

type Coordinates is record
   X, Y, Z : Float;
end record;

type Hidden_Coordinates is new Coordinates;   --  FLAG

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

Example

Outer : for J in S1'Range loop
   for K in S2'Range loop
      if S1 (J) = S2 (K) then
         Detected := True;
         exit Outer;                     --  FLAG
      end if;
   end loop;
end loop Outer;

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

Example

type Rec is record
   C1 : Integer;
   C2 : Float;
end record;

function "<" (Left, Right : Rec) return Boolean;    --  FLAG

10.4.8. Slices

Flag all uses of array slicing

This rule has no parameters.

Example

procedure Proc (S : in out String; L, R : Positive) is
   Tmp : String := S (L .. R);        --  FLAG
begin

10.4.9. Universal_Ranges

Flag discrete ranges that are a part of an index constraint, constrained array definition, or for-loop parameter specification, and whose bounds are both of type universal_integer. Ranges that have at least one bound of a specific type (such as 1 .. N, where N is a variable or an expression of non-universal type) are not flagged.

This rule has no parameters.

Example

L : Positive := 1;

S1 : String (L .. 10);
S2 : String (1 .. 10);     --  FLAG