4 SPARK Ada Rules

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

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

4.2 Expanded_Loop_Exit_Names

Flag all expanded loop names in exit statements.

This rule has no parameters.

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

4.4 Non_Tagged_Derived_Types

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

This rule has no parameters.

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

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

4.7 Slices

Flag all uses of array slicing

This rule has no parameters.

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