[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 | ||
4.2 Expanded_Loop_Exit_Names | ||
4.3 Non_SPARK_Attributes | ||
4.4 Non_Tagged_Derived_Types | ||
4.5 Outer_Loop_Exits | ||
4.6 Overloaded_Operators | ||
4.7 Slices | ||
4.8 Universal_Ranges |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [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.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Expanded_Loop_Exit_Names
Flag all expanded loop names in exit
statements.
This rule has no parameters.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [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.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Non_Tagged_Derived_Types
Flag all derived type declarations that do not have a record extension part.
This rule has no parameters.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [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.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [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.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Slices
Flag all uses of array slicing
This rule has no parameters.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [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.
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by root on February 6, 2012 using texi2html 1.82.