Next: List of Rules, Previous: Metrics-Related Rules [Contents][Index]
The rules in this chapter can be used to enforce compliance with the Ada subset allowed by the SPARK tools.
• Boolean_Relational_Operators: | ||
• Expanded_Loop_Exit_Names: | ||
• Non_SPARK_Attributes: | ||
• Non_Tagged_Derived_Types: | ||
• Outer_Loop_Exits: | ||
• Overloaded_Operators: | ||
• Slices: | ||
• Universal_Ranges: |
Next: Expanded_Loop_Exit_Names, Up: SPARK Ada Rules [Contents][Index]
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.
Next: Non_SPARK_Attributes, Previous: Boolean_Relational_Operators, Up: SPARK Ada Rules [Contents][Index]
Expanded_Loop_Exit_Names
Flag all expanded loop names in exit
statements.
This rule has no parameters.
Next: Non_Tagged_Derived_Types, Previous: Expanded_Loop_Exit_Names, Up: SPARK Ada Rules [Contents][Index]
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.
Next: Outer_Loop_Exits, Previous: Non_SPARK_Attributes, Up: SPARK Ada Rules [Contents][Index]
Non_Tagged_Derived_Types
Flag all derived type declarations that do not have a record extension part.
This rule has no parameters.
Next: Overloaded_Operators, Previous: Non_Tagged_Derived_Types, Up: SPARK Ada Rules [Contents][Index]
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.
Next: Slices, Previous: Outer_Loop_Exits, Up: SPARK Ada Rules [Contents][Index]
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.
Next: Universal_Ranges, Previous: Overloaded_Operators, Up: SPARK Ada Rules [Contents][Index]
Slices
Flag all uses of array slicing
This rule has no parameters.
Previous: Slices, Up: SPARK Ada Rules [Contents][Index]
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.
Previous: Slices, Up: SPARK Ada Rules [Contents][Index]