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