asis_2019.0.0_3ca32fa2/tools/gnatcheck/gnatcheck-rules-default.ads

------------------------------------------------------------------------------
--                                                                          --
--                          GNATCHECK COMPONENTS                            --
--                                                                          --
--              G N A T C H E C K . R U L E S . D E F A U L T               --
--                                                                          --
--                                 S p e c                                  --
--                                                                          --
--                     Copyright (C) 2004-2017, AdaCore                     --
--                                                                          --
-- GNATCHECK  is  free  software;  you can redistribute it and/or modify it --
-- under terms of the  GNU  General Public License as published by the Free --
-- Software Foundation;  either version 2, or ( at your option)  any  later --
-- version.  GNATCHECK  is  distributed in the hope that it will be useful, --
-- but  WITHOUT  ANY  WARRANTY;   without  even  the  implied  warranty  of --
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General --
-- Public License for more details.  You should have received a copy of the --
-- GNU  General Public License distributed with GNAT; see file  COPYING. If --
-- not,  write to the  Free Software Foundation,  51 Franklin Street, Fifth --
-- Floor, Boston, MA 02110-1301, USA.                                       --
--                                                                          --
-- GNATCHECK is maintained by AdaCore (http://www.adacore.com).             --
--                                                                          --
------------------------------------------------------------------------------

--  This package defines the default set of rules for gnatcheck. Use ???
--  to extend the set of rules

pragma Ada_2012;

package Gnatcheck.Rules.Default is

   --------------------------------
   -- Abstract_Type_Declarations --
   --------------------------------

   --  The use of abstract types are detected. In case of an abstract private
   --  type, both private and full type declarations are detected.

   type Abstract_Type_Declarations_Rule_Type is new Rule_Template with
     null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Abstract_Type_Declarations_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is an abstract type declaration

   procedure Init_Rule (Rule : in out Abstract_Type_Declarations_Rule_Type);

   Abstract_Type_Declarations_Rule :
     aliased Abstract_Type_Declarations_Rule_Type;

   ------------------------
   -- Anonymous_Subtypes --
   ------------------------

   --  Any use of an anonymous subtype is detected.

   --  A use of an anonymous subtype is any use of a construct
   --  'subtype_mark constraint' different from immediately within a subtype
   --  declaration. Any use of range different from the situation when this
   --  range is a constraint used immediately within a subtype declaration is
   --  also considered as the use of an anonymous subtype and should be
   --  detected

   type Anonymous_Subtypes_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Anonymous_Subtypes_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is an abstract type declaration

   procedure Init_Rule (Rule : in out Anonymous_Subtypes_Rule_Type);

   Anonymous_Subtypes_Rule : aliased Anonymous_Subtypes_Rule_Type;

   ------------
   -- Blocks --
   ------------

   --  Block statements are detected.

   type Blocks_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Blocks_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is a block statement

   procedure Init_Rule (Rule : in out Blocks_Rule_Type);

   Blocks_Rule : aliased Blocks_Rule_Type;

   ----------------------------------
   -- Boolean_Relational_Operators --
   ----------------------------------

   --  According to the definition of the Spark language, relation operations
   --  <, >, <=, >=, = and /= cannot be used for the type Boolean.

   --  Calls to predefined relation operators (<, >, <=, >=, = and /=) of
   --  the predefined Boolean type are detected.

   --  Calls to predefined relation operations of any type derived from
   --  Standard.Boolean are not detected.

   --  Calls to user-defined functions with these designators are not detected

   --  The use of an operation that is a renaming of a predefined relation
   --  operation for Standard.Boolean is not detected

   type Boolean_Relational_Operators_Rule_Type is new Rule_Template with
     null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Boolean_Relational_Operators_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  If Element represents any of the comparison operators listed above,
   --  checks that the argument of this operation are both of the type
   --  Standard.Boolean

   procedure Init_Rule (Rule : in out Boolean_Relational_Operators_Rule_Type);

   Boolean_Relational_Operators_Rule :
     aliased Boolean_Relational_Operators_Rule_Type;

   ------------------------
   -- Ceiling_Violations --  turned off!!! --
   ------------------------

   --  Any caller to a protected operation should have the priority not higher
   --  then the called protected operation.

   --  The situations when a protected operation is called by a higher priority
   --  task is detected.

   --  At the moment, the detection of violations of ceiling priority
   --  consistency is performed with the following limitations:
   --
   --  - We consider only pragmas Priority and Interrupt_Priority as means to
   --    define a task/protected operation priority. We do not consider the
   --    effect of using Ada.Dynamic_Priorities.Set_Priority procedure;
   --
   --  - We consider only base task priorities, and no priority inheritance.
   --    That is, we do not make a difference between calls issued during task
   --    activation and execution of the sequence of statements from task body;
   --
   --  - Any situation when the priority of protected operation caller is set
   --    by a dynamic expression (that is, the corresponding Priority or
   --    Interrupt_Priority pragma has a non-static expression as an argument)
   --    we treat as a priority inconsistency (and, therefore, detect this
   --    situation).
   --
   --  At the moment the notion of the main subprogram is not implemented in
   --  gnatcheck, so any pragma Priority in a library level subprogram body
   --  (in case if this subprogram Can_Be_Main_Program) changes the priority
   --  of an environment task. So if we have more than one such pragma in the
   --  set of processed sources, the pragma that is processed last, defines the
   --  priority of an environment task.

--   type Ceiling_Violations_Rule_Type is new Global_Rule_Template with
--     null record;

--   procedure Collect_Global_Info_Pre_Op
--     (Rule    : in out Ceiling_Violations_Rule_Type;
--      Element :        Asis.Element;
--      Control : in out Traverse_Control;
--      State   : in out Rule_Traversal_State);
   --  Tries to detect the priority of the given scope from pragmas Priority
   --  and Interrupt_Priority (if any).

--   procedure Analyze_Global_Structure
--     (Rule : Ceiling_Violations_Rule_Type);
   --  If for the given node the priority is not defined, computes the priority
   --  from the call graph: for a protected operation, takes the priority from
   --  the node corresponding to protected definition, for other nodes, or in
   --  case if there is no priority setting pragmas applied to a protected
   --  definition, "inherits" the priority of an enclosing scope.

--   procedure Check_Global_Structure_Node
--     (Rule     :     Ceiling_Violations_Rule_Type;
--      N        :     Gnatcheck.Global_State.GS_Node_Id;
--      Detected : out Boolean);
   --  If the given call graph node represents a protected operation, checks
   --  that all the callers have priorities not higher, then the protected
   --  operation. Dynamic priority is considered as a highest priority level.

--   procedure Init_Rule (Rule : in out Ceiling_Violations_Rule_Type);

--   Ceiling_Violations_Rule : aliased Ceiling_Violations_Rule_Type;

   ----------------------------------
   -- Controlled_Type_Declarations --
   ----------------------------------

   --  Declarations of controlled types are detected.

   --  A declaration of a private type is detected if its full declaration
   --  defines a controlled type.

   --  A declaration of a derived type is detected if its ancestor type is
   --  controlled.

   --  Subtype declarations are not detected.

   --  The declaration of a type that itself is not a descendant of a type
   --  declared  in Ada.Finalization but has a controlled component is not
   --  detected

   type Controlled_Type_Declarations_Rule_Type is new Rule_Template with
     null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Controlled_Type_Declarations_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is a declaration of a controlled type as described
   --  above

   procedure Init_Rule (Rule : in out Controlled_Type_Declarations_Rule_Type);

   Controlled_Type_Declarations_Rule :
     aliased Controlled_Type_Declarations_Rule_Type;

   ----------------------------
   -- Declarations_In_Blocks --
   ----------------------------

   --  Block statements with local declarations are detected.

   --  A declare block with an empty declarative_part or with a declarative
   --  part containing only pragmas and/or use clauses is not detected.

   type Declarations_In_Blocks_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Declarations_In_Blocks_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is a block statement containing local declarations.

   procedure Init_Rule (Rule : in out Declarations_In_Blocks_Rule_Type);

   Declarations_In_Blocks_Rule : aliased Declarations_In_Blocks_Rule_Type;

   ------------------------
   -- Default_Parameters --
   ------------------------

   --  Default expressions for subprogram parameters are detected.
   --  Parameter declarations of formal and generic subprograms are also
   --  considered

   type Default_Parameters_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Default_Parameters_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is a parameter specification containing a default
   --  initialization expression

   procedure Init_Rule (Rule : in out Default_Parameters_Rule_Type);

   Default_Parameters_Rule : aliased Default_Parameters_Rule_Type;

   ---------------------------
   -- Discriminated_Records --
   ---------------------------

   --  Declarations of record types with discriminants are detected.

   --  Only the declarations of record and record extension types are detected.
   --  Incomplete, formal, private, derived and private extension type
   --  declarations are not detected. Task and protected type declarations also
   --  are not detected.

   type Discriminated_Records_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Discriminated_Records_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is known discriminant part in a record or record
   --  extension definition

   procedure Init_Rule (Rule : in out Discriminated_Records_Rule_Type);

   Discriminated_Records_Rule : aliased Discriminated_Records_Rule_Type;

   ------------------------------
   -- Expanded_Loop_Exit_Names --
   ------------------------------

   --  According to the definition of the Spark language, the loop name in an
   --  exit statement should be only a simple loop name, expanded names are not
   --  allowed.

   --  Expanded loop name in an exit statement is detected

   type Expanded_Loop_Exit_Names_Rule_Type is new Rule_Template
     with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Expanded_Loop_Exit_Names_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  If Element is an exit statement, checks if the statement contains a loop
   --  name and if it does, check that this is a simple name

   procedure Init_Rule (Rule : in out Expanded_Loop_Exit_Names_Rule_Type);

   Expanded_Loop_Exit_Names_Rule : aliased Expanded_Loop_Exit_Names_Rule_Type;

   ---------------------------
   -- Float_Equality_Checks --
   ---------------------------

   --  Calls to the predefined equality operations for floating point types
   --  are detected

   --  Both "=" and "/=" operations are checked.

   --  A floating point type here is a type declared with floating point
   --  definition or a type derived from a floating point type

   --  User-defined equality operations are not detected.

   --  "=" and "/=" operations for fixed point types are not detected

   type Float_Equality_Checks_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Float_Equality_Checks_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks if Element is a name of a predefined "=" or "/=" operator from
   --  a (function) call with float arguments

   procedure Init_Rule (Rule : in out Float_Equality_Checks_Rule_Type);

   Float_Equality_Checks_Rule : aliased Float_Equality_Checks_Rule_Type;

   ---------------------
   -- GOTO_Statements --
   ---------------------

   --  goto statements are detected.

   type GOTO_Statements_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out GOTO_Statements_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is a goto statement

   procedure Init_Rule (Rule : in out GOTO_Statements_Rule_Type);

   GOTO_Statements_Rule : aliased GOTO_Statements_Rule_Type;

   ----------------------
   -- Improper_Returns --
   ----------------------

   --  A return statement in a procedure body is detected

   --  The situation when there is more than exactly one return statement in a
   --  function body is detected (diagnostic message is generated for all the
   --  return statements except the first one).

   --  Should we should split this rule into two rules - one for procedures,
   --  and another one for functions?

   type Improper_Returns_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Improper_Returns_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  If Element is a return statement, checks that the enclosing subprogram
   --  body is not a procedure body, and if it is a function body, checks that
   --  this is the first return statement in the body.

   procedure Init_Rule (Rule : in out Improper_Returns_Rule_Type);

   Improper_Returns_Rule : aliased Improper_Returns_Rule_Type;

   -----------------------------------------
   -- Improperly_Called_Protected_Entries --   turned off!!! --
   -----------------------------------------

   --  There are situations when it is required that the maximal number of
   --  tasks calling a given protected entry is 1.

   --  Protected entries that can be called more than one task are detected.

--   type Improperly_Called_Protected_Entries_Rule_Type is
--     new Global_Rule_Template with null record;

--   procedure Check_Global_Structure_Node
--     (Rule     :     Improperly_Called_Protected_Entries_Rule_Type;
--      N        :     Gnatcheck.Global_State.GS_Node_Id;
--      Detected : out Boolean);
--   --  Checks if there are more than one task calling the given protected
--   --  entry.

--   procedure Init_Rule
--     (Rule : in out Improperly_Called_Protected_Entries_Rule_Type);

--   Improperly_Called_Protected_Entries_Rule :
--     aliased Improperly_Called_Protected_Entries_Rule_Type;

   -----------------------
   -- Limited_Renamings --
   -----------------------

   --  This rule combines a part of the SPARK limitations imposed on renamings.
   --  It is formulated for renaming declarations only, not for the use of
   --  renamed entities. The following situations should be detected:

   --  Syntax of renaming declarations: all forms of  renaming declarations
   --  except package and subprogram renaming declarations should be detected.

   --  Renamed entities: only subprograms declared immediately within package
   --  specs and only child packages can be renamed. All other cases of
   --  subprogram and package renamings should be detected.

   --  Limitations on new and old names: the name after RENAMES should have
   --  the form package_name.entity_name, the new name should be exactly the
   --  same as entity_name, entity_name should not itself be detected by a
   --  renaming declaration. Moreover, in case of a subprogram renaming, the
   --  new and the old profiles should be the same (the same parameter and
   --  subtype names should be used). All the renamings that do not follow
   --  these rules should be detected.

   --  Placement of renamings. According to the definition of SPARK, the
   --  following restrictions are imposed on the placement of renaming
   --  declarations:
   --
   --  for subprogram renamings (that are not operator renamings):
   --  - if the package where the subprogram is declared is a local package,
   --    renaming is allowed immediately after the declaration of this
   --    package;
   --  - if the package where the subprogram is declared is a library-level
   --    package, renaming is allowed at the start of the body of a library
   --    package (or library subprogram) that "withes" this package;
   --
   --  for operator renamings: the same is allowed as for subprogram renamings
   --  plus renamings are allowed at the start of the visible or private part
   --  of the library package that "withes" the package where the operator is
   --  declared;
   --
   --  for package renamings: the renaming of a (child!) package is allowed
   --  only immediately within a library package or library subprogram that
   --  "withes" this package;
   --
   --  All the other cases of renaming declaration placement should be
   --  detected.
   --
   --  Note that the rules about allowed renaming placement are taken from the
   --  definition of the SPARK subset. This definition uses the following
   --  wording: "at the start of the body", "at the start of the visible
   --  (private) part", and it the same time the SPARK book contains examples
   --  where an (allowed) renaming follows an object declaration. So we do
   --  not check that renamings precede all the non-renaming declarations.

   --  All the things stated above are checked and detected in the order given.
   --  If some feature is detected for a renaming declaration, all the other
   --  things are not checked for this renaming declaration

   --  Current implementation limitation: an the moment this rule is not
   --  completely checked for renaming of predefined operators.

   type Limited_Renamings_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Limited_Renamings_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  If Element is a renaming declaration, checks the rules stated above in
   --  the order given. As soon as the first rule violation is detected, stops
   --  further processing

   procedure Init_Rule (Rule : in out Limited_Renamings_Rule_Type);

   Limited_Renamings : aliased Limited_Renamings_Rule_Type;

   -------------------------------
   -- Library_Level_Subprograms --
   -------------------------------

   --  Library level subprograms (including subprogram instantiations) are
   --  detected.

   type Library_Level_Subprograms_Rule_Type is new Rule_Template
     with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Library_Level_Subprograms_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is a library_Level subprogram

   procedure Init_Rule (Rule : in out Library_Level_Subprograms_Rule_Type);

   Library_Level_Subprograms_Rule :
     aliased Library_Level_Subprograms_Rule_Type;

   --------------------
   -- Local_Packages --
   --------------------

   --  Local packages in package and generic package specs are detected.

   --  Local packages in bodies are not detected

   type Local_Packages_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Local_Packages_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is a package spec enclosed in another (generic)
   --  package spec

   procedure Init_Rule (Rule : in out Local_Packages_Rule_Type);

   Local_Packages_Rule : aliased Local_Packages_Rule_Type;

   -----------------------------------------------
   -- Multiple_Entries_In_Protected_Definitions --
   -----------------------------------------------

   --  At most one entry is allowed in protected object (or in protected type).
   --  This is the requirement from the Ravenscar Profile.

   --  The situations when a protected definition defines more than one entry
   --  are detected (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
   --  counted

   type Multiple_Entries_In_Protected_Definitions_Rule_Type is new
     Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Multiple_Entries_In_Protected_Definitions_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  If Element is An_Entry_Declaration, checks if the enclosing element is
   --  A_Protected_Definition and if there are some other entries declared for
   --  the given protected object or type. In case if the protected type/object
   --  has more than one entry, the diagnostic message is generated the all but
   --  the first entry.

   procedure Init_Rule
     (Rule : in out Multiple_Entries_In_Protected_Definitions_Rule_Type);

   Multiple_Entries_In_Protected_Definitions_Rule :
     aliased Multiple_Entries_In_Protected_Definitions_Rule_Type;

   ------------------
   -- Name_Clashes --
   ------------------

   --  Detect that some names are not used as defining identifiers. To activate
   --  this rule, one have to provide a reference to a dictionary file as a
   --  rule parameter(s), more than one dictionary file can be specified. If
   --  no dictionary file is set, nothing is detected.

   --  Only defining identifiers are detected. but not references. The check is
   --  not case-sensitive.

   --  See Gnatcheck.Name_Dictionary (spec) for the description of the
   --  dictionary structure

   type Name_Clashes_Rule_Type is new Rule_Template with null record;

   overriding procedure Activate_In_Test_Mode
     (Rule : in out Name_Clashes_Rule_Type);
   --  Activates the rule with the dictionary containing "one", "two" and
   --  "three"

   procedure Rule_Check_Pre_Op
     (Rule    : in out Name_Clashes_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  If Element is a defining identifier, checks if it is not in the
   --  dictionary of the forbidden names

   procedure Init_Rule (Rule : in out Name_Clashes_Rule_Type);

   overriding procedure Process_Rule_Parameter
     (Rule       : in out Name_Clashes_Rule_Type;
      Param      :        String;
      Enable     :        Boolean;
      Defined_At :        String);
   --  If Enable is OFF, this procedure does nothing. If Enable is ON, treats
   --  Param as a name of the dictionary file. Scans this file and fill in the
   --  dictionary of forbidden names. The rule is turned into 'Enabled" state
   --  if the dictionary contains at least one entry. (Note that this entry may
   --  be created by the previous call to this routine)
   --
   --  We may want to have more sophisticated way of controlling the dictionary
   --  of forbidden names. For example, the option "-RRestrict_Name_Space:dict"
   --  may remove from the dictionary of forbidden names the names that are
   --  stated in 'dict'
   --
   --  No warning about parameter redefinition is issued by this procedure
   --  because more than one dictionary file is allowed.

   procedure XML_Rule_Help
     (Rule  : Name_Clashes_Rule_Type;
      Level : Natural);
   --  Generates the field tag

   overriding function Rule_Option
     (Rule          : Name_Clashes_Rule_Type;
      Template_Kind : Template_Coding_Standard_Kinds)
      return          String;
   --  For Template_All_ON  pints out rule option in the format
   --  "-- +R rule_name : dictionary" because we cannot activate this rule in
   --  the coding standard template because it requires a real dictionary file
   --  as a parameter

   overriding function More_Rule_Comment
     (Rule          : Name_Clashes_Rule_Type;
      Template_Kind : Template_Coding_Standard_Kinds)
      return String;
   --  Adds the note that the rule may be activated only with a real dictionary
   --  file as a parameter.

   Name_Clashes_Rule : aliased Name_Clashes_Rule_Type;

   ------------------------------
   -- Non_Qualified_Aggregates --
   ------------------------------

   --  According to the definition of the Spark language, all the aggregates
   --  should be explicitly qualified

   --  Non-qualified aggregates are detected

   --  A non qualified aggregate is an aggregate that is not an immediate
   --  component of a qualified expression.

   --  A string literal is not considered as aggregate by this rule, but an
   --  array aggregate of some string type is considered as a normal aggregate.

   type Non_Qualified_Aggregates_Rule_Type is new Rule_Template
     with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Non_Qualified_Aggregates_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  If Element is an aggregate, checks that the enclosing element is
   --  of A_Qualified_Expression kind

   procedure Init_Rule (Rule : in out Non_Qualified_Aggregates_Rule_Type);

   Non_Qualified_Aggregates_Rule : aliased Non_Qualified_Aggregates_Rule_Type;

   --------------------------
   -- Non_SPARK_Attributes --
   --------------------------

   --  The definition of the Spark language defines a subset  of Ada 95
   --  attribute designators that can be used in Spark programs.

   --  The use of any attribute that is not from this subset is detected

   type Non_SPARK_Attributes_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Non_SPARK_Attributes_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  If Element is an attribute, checks that this is the attribute from the
   --  Spark subset of Ada 95 attributes

   procedure Init_Rule (Rule : in out Non_SPARK_Attributes_Rule_Type);

   Non_SPARK_Attributes_Rule : aliased Non_SPARK_Attributes_Rule_Type;

   ------------------------------
   -- Non_Tagged_Derived_Types --
   ------------------------------

   --  According to the definition of the Spark language, "derived types are
   --  only used for type extensions". Derived type declarations that do not
   --  have a record extension part are detected

   type Non_Tagged_Derived_Types_Rule_Type is new Rule_Template with
     null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Non_Tagged_Derived_Types_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks if Element is of A_Derived_Type_Definition kind

   procedure Init_Rule (Rule : in out Non_Tagged_Derived_Types_Rule_Type);

   Non_Tagged_Derived_Types_Rule : aliased Non_Tagged_Derived_Types_Rule_Type;

   ----------------------
   -- Outer_Loop_Exits --
   ----------------------

   --  According to the definition of the Spark language, an exit statement can
   --  transfer control only out of the immediately enclosing loop statement.
   --  An exit statement containing a loop name that is not the name of the
   --  immediately enclosing loop statement is detected.

   type Outer_Loop_Exits_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Outer_Loop_Exits_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is an exit statement with a loop name that does not
   --  denote an immediately enclosing loop

   procedure Init_Rule (Rule : in out Outer_Loop_Exits_Rule_Type);

   Outer_Loop_Exits_Rule : aliased Outer_Loop_Exits_Rule_Type;

   --------------------------
   -- Overloaded_Operators --
   --------------------------

   --  According to the definition of the Spark language, the designator of a
   --  function cannot be an operator, because operator overloading is not
   --  allowed in Spark.

   --  A function declaration with an operator symbol as a defining designator
   --  is detected.

   --  A function body is detected only if the body does not have a separate
   --  spec

   --  Formal functions are also considered for this rule

   --  For a renaming declarations, only renaming-as-declaration is detected

   type Overloaded_Operators_Rule_Type is new Rule_Template with
     null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Overloaded_Operators_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is a defining operator symbol.

   procedure Init_Rule (Rule : in out Overloaded_Operators_Rule_Type);

   Overloaded_Operators_Rule : aliased Overloaded_Operators_Rule_Type;

   ------------
   -- Slices --
   ------------

   --  The definition of the Spark language does not have a slice as a variant
   --  of the name syntax structure.

   --  The use of slices is detected.

   type Slices_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Slices_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is a slice

   procedure Init_Rule (Rule : in out Slices_Rule_Type);

   Slices_Rule : aliased Slices_Rule_Type;

   ---------------------------------
   -- Unconstrained_Array_Returns --
   ---------------------------------

   --  Functions returning unconstrained arrays are detected

   --  Functions declarations, function bodies (and body stubs) having no
   --  separate declarations and function instantiations are detected. Function
   --  calls are not detected. Function renamings are not detected.
   --
   --  The rule has the following parameters:
   --
   --  * for +R option:
   --
   --       Except_String - if this parameter is specified, functions that
   --                       return predefined type String or any type derived
   --                       from it (directly or indirectly) are not flagged

   type Unconstrained_Array_Returns_Rule_Type is new
     Rule_With_Exceptions_Template (1) with null record;

   overriding procedure Activate_In_Test_Mode
     (Rule : in out Unconstrained_Array_Returns_Rule_Type);
   --  Activates the rule with Except_String parameter.

   function Exception_Name
     (Rule      : Unconstrained_Array_Returns_Rule_Type;
      Exc_Index : Exception_Index)
      return      String;

   function Exception_Number
     (Rule     : Unconstrained_Array_Returns_Rule_Type;
      Exc_Name : String)
      return     Exception_Numbers;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Unconstrained_Array_Returns_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is the declaration of a function returning an
   --  unconstrained array type

   procedure Init_Rule (Rule : in out Unconstrained_Array_Returns_Rule_Type);

   Unconstrained_Array_Returns_Rule :
     aliased Unconstrained_Array_Returns_Rule_Type;

   ----------------------
   -- Universal_Ranges --
   ----------------------

   --  In the Spark language, ranges with the bounds of universal_integer
   --  type are not allowed in index constraints, constrained array definitions
   --  and FOR-loop parameter specifications.

   --  Discrete ranges that are a part of index constrains, constrained array
   --  definition or FOR-loop parameter specification, and that have both
   --  bounds of the universal type integer type are detected. 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 detected.

   type Universal_Ranges_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Universal_Ranges_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  If Element if of A_Discrete_Simple_Expression_Range kind and its
   --  enclosing Element is either A_Loop_Parameter_Specification, or
   --  An_Index_Constraint, or A_Discrete_Subtype_Definition, checks that
   --  both bounds are of universal_integer type.

   procedure Init_Rule (Rule : in out Universal_Ranges_Rule_Type);

   Universal_Ranges_Rule : aliased Universal_Ranges_Rule_Type;

   ------------------------
   -- Unused_Subprograms -- turned off!!! --
   ------------------------

   --  Unused subprograms are detected.

   --  In some sense this rule duplicates the functionality of gnatelim

   --  For the moment the main purpose of this rule is to use gnatelim tests
   --  to check the gnatcheck call graph.

   --  ??? What kinds of callable entities should be checked here?

--   type Unused_Subprograms_Rule_Type is new Global_Rule_Template with
--     null record;

--   procedure Analyze_Global_Structure (Rule : Unused_Subprograms_Rule_Type);
   --  Sets Is_Used flags by analyzing the Call Graph entry points and call
   --  chains. Does not detect any rule violation.

--   procedure Check_Global_Structure_Node
--     (Rule     :     Unused_Subprograms_Rule_Type;
--      N        :     Gnatcheck.Global_State.GS_Node_Id;
--      Detected : out Boolean);
   --  Checks if the given call graph node is called by some other (used!)
   --  node.

--   procedure Init_Rule (Rule : in out Unused_Subprograms_Rule_Type);

--   Unused_Subprograms_Rule : aliased Unused_Subprograms_Rule_Type;

   -------------------------
   -- USE_PACKAGE_Clauses --
   -------------------------

   --  Use package clauses are detected. Use type clauses are not detected.

   type USE_PACKAGE_Clauses_Rule_Type is new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out USE_PACKAGE_Clauses_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);
   --  Checks that Element is a use package clause

   procedure Init_Rule (Rule : in out USE_PACKAGE_Clauses_Rule_Type);

   USE_PACKAGE_Clauses_Rule : aliased USE_PACKAGE_Clauses_Rule_Type;

   ----------------------------------------------
   -- Volatile_Objects_Without_Address_Clauses --
   ----------------------------------------------

   --  A volatile object that does not have an address clause applied to it is
   --  detected
   --
   --  Only variable declarations are checked. This rule treats an object as a
   --  volatile object if pragma or aspect Volatile is applied to the object
   --  or to its type, if the object is atomic or if the GNAT compiler
   --  considers this object as volatile because of some code generation
   --  reasons.

   type Volatile_Objects_Without_Address_Clauses_Rule_Type is
     new Rule_Template with null record;

   procedure Rule_Check_Pre_Op
     (Rule    : in out Volatile_Objects_Without_Address_Clauses_Rule_Type;
      Element :        Asis.Element;
      Control : in out Traverse_Control;
      State   : in out Rule_Traversal_State);

   procedure Init_Rule
     (Rule : in out Volatile_Objects_Without_Address_Clauses_Rule_Type);

   Volatile_Objects_Without_Address_Clauses_Rule :
     aliased Volatile_Objects_Without_Address_Clauses_Rule_Type;

end Gnatcheck.Rules.Default;