3. Implementation Defined Aspects
Ada defines (throughout the Ada 2012 reference manual, summarized in Annex K) a set of aspects that can be specified for certain entities. These language defined aspects are implemented in GNAT in Ada 2012 mode and work as described in the Ada 2012 Reference Manual.
In addition, Ada 2012 allows implementations to define additional aspects whose meaning is defined by the implementation. GNAT provides a number of these implementation-defined aspects which can be used to extend and enhance the functionality of the compiler. This section of the GNAT reference manual describes these additional aspects.
Note that any program using these aspects may not be portable to other compilers (although GNAT implements this set of aspects on all platforms). Therefore if portability to other compilers is an important consideration, you should minimize the use of these aspects.
Note that for many of these aspects, the effect is essentially similar to the use of a pragma or attribute specification with the same name applied to the entity. For example, if we write:
type R is range 1 .. 100
with Value_Size => 10;
then the effect is the same as:
type R is range 1 .. 100;
for R'Value_Size use 10;
and if we write:
type R is new Integer
with Shared => True;
then the effect is the same as:
type R is new Integer;
pragma Shared (R);
In the documentation below, such cases are simply marked as being boolean aspects equivalent to the corresponding pragma or attribute definition clause.
3.1. Aspect Abstract_State
This aspect is equivalent to pragma Abstract_State.
3.2. Aspect Always_Terminates
This boolean aspect is equivalent to pragma Always_Terminates.
3.3. Aspect Annotate
There are three forms of this aspect (where ID is an identifier, and ARG is a general expression), corresponding to pragma Annotate.
- Annotate => ID
Equivalent to
pragma Annotate (ID, Entity => Name);
- Annotate => (ID)
Equivalent to
pragma Annotate (ID, Entity => Name);
- Annotate => (ID ,ID {, ARG})
Equivalent to
pragma Annotate (ID, ID {, ARG}, Entity => Name);
3.4. Aspect Async_Readers
This boolean aspect is equivalent to pragma Async_Readers.
3.5. Aspect Async_Writers
This boolean aspect is equivalent to pragma Async_Writers.
3.6. Aspect Constant_After_Elaboration
This aspect is equivalent to pragma Constant_After_Elaboration.
3.7. Aspect Contract_Cases
This aspect is equivalent to pragma Contract_Cases, the sequence of clauses being enclosed in parentheses so that syntactically it is an aggregate.
3.8. Aspect Depends
This aspect is equivalent to pragma Depends.
3.9. Aspect Default_Initial_Condition
This aspect is equivalent to pragma Default_Initial_Condition.
3.10. Aspect Dimension
The Dimension
aspect is used to specify the dimensions of a given
subtype of a dimensioned numeric type. The aspect also specifies a symbol
used when doing formatted output of dimensioned quantities. The syntax is:
with Dimension =>
([Symbol =>] SYMBOL, DIMENSION_VALUE {, DIMENSION_Value})
SYMBOL ::= STRING_LITERAL | CHARACTER_LITERAL
DIMENSION_VALUE ::=
RATIONAL
| others => RATIONAL
| DISCRETE_CHOICE_LIST => RATIONAL
RATIONAL ::= [-] NUMERIC_LITERAL [/ NUMERIC_LITERAL]
This aspect can only be applied to a subtype whose parent type has
a Dimension_System
aspect. The aspect must specify values for
all dimensions of the system. The rational values are the powers of the
corresponding dimensions that are used by the compiler to verify that
physical (numeric) computations are dimensionally consistent. For example,
the computation of a force must result in dimensions (L => 1, M => 1, T => -2).
For further examples of the usage
of this aspect, see package System.Dim.Mks
.
Note that when the dimensioned type is an integer type, then any
dimension value must be an integer literal.
3.11. Aspect Dimension_System
The Dimension_System
aspect is used to define a system of
dimensions that will be used in subsequent subtype declarations with
Dimension
aspects that reference this system. The syntax is:
with Dimension_System => (DIMENSION {, DIMENSION});
DIMENSION ::= ([Unit_Name =>] IDENTIFIER,
[Unit_Symbol =>] SYMBOL,
[Dim_Symbol =>] SYMBOL)
SYMBOL ::= CHARACTER_LITERAL | STRING_LITERAL
This aspect is applied to a type, which must be a numeric derived type
(typically a floating-point type), that
will represent values within the dimension system. Each DIMENSION
corresponds to one particular dimension. A maximum of 7 dimensions may
be specified. Unit_Name
is the name of the dimension (for example
Meter
). Unit_Symbol
is the shorthand used for quantities
of this dimension (for example m
for Meter
).
Dim_Symbol
gives
the identification within the dimension system (typically this is a
single letter, e.g. L
standing for length for unit name Meter
).
The Unit_Symbol
is used in formatted output of dimensioned quantities.
The Dim_Symbol
is used in error messages when numeric operations have
inconsistent dimensions.
GNAT provides the standard definition of the International MKS system in
the run-time package System.Dim.Mks
. You can easily define
similar packages for cgs units or British units, and define conversion factors
between values in different systems. The MKS system is characterized by the
following aspect:
type Mks_Type is new Long_Long_Float with
Dimension_System => (
(Unit_Name => Meter, Unit_Symbol => 'm', Dim_Symbol => 'L'),
(Unit_Name => Kilogram, Unit_Symbol => "kg", Dim_Symbol => 'M'),
(Unit_Name => Second, Unit_Symbol => 's', Dim_Symbol => 'T'),
(Unit_Name => Ampere, Unit_Symbol => 'A', Dim_Symbol => 'I'),
(Unit_Name => Kelvin, Unit_Symbol => 'K', Dim_Symbol => '@'),
(Unit_Name => Mole, Unit_Symbol => "mol", Dim_Symbol => 'N'),
(Unit_Name => Candela, Unit_Symbol => "cd", Dim_Symbol => 'J'));
Note that in the above type definition, we use the at
symbol (@
) to
represent a theta character (avoiding the use of extended Latin-1
characters in this context).
See section ‘Performing Dimensionality Analysis in GNAT’ in the GNAT Users Guide for detailed examples of use of the dimension system.
3.12. Aspect Disable_Controlled
The aspect Disable_Controlled
is defined for controlled record types. If
active, this aspect causes suppression of all related calls to Initialize
,
Adjust
, and Finalize
. The intended use is for conditional compilation,
where for example you might want a record to be controlled or not depending on
whether some run-time check is enabled or suppressed.
3.13. Aspect Effective_Reads
This aspect is equivalent to pragma Effective_Reads.
3.14. Aspect Effective_Writes
This aspect is equivalent to pragma Effective_Writes.
3.15. Aspect Exceptional_Cases
This aspect may be specified for procedures and functions with side effects; it can be used to list exceptions that might be propagated by the subprogram with side effects in the context of its precondition, and associate them with a specific postcondition.
For the syntax and semantics of this aspect, see the SPARK 2014 Reference Manual, section 6.1.9.
3.16. Aspect Extensions_Visible
This aspect is equivalent to pragma Extensions_Visible.
3.17. Aspect Favor_Top_Level
This boolean aspect is equivalent to pragma Favor_Top_Level.
3.18. Aspect Ghost
This aspect is equivalent to pragma Ghost.
3.19. Aspect Ghost_Predicate
This aspect introduces a subtype predicate that can reference ghost entities. The subtype cannot appear as a subtype_mark in a membership test.
For the detailed semantics of this aspect, see the entry for subtype predicates in the SPARK Reference Manual, section 3.2.4.
3.20. Aspect Global
This aspect is equivalent to pragma Global.
3.21. Aspect Initial_Condition
This aspect is equivalent to pragma Initial_Condition.
3.22. Aspect Initializes
This aspect is equivalent to pragma Initializes.
3.23. Aspect Inline_Always
This boolean aspect is equivalent to pragma Inline_Always.
3.24. Aspect Invariant
This aspect is equivalent to pragma Invariant. It is a
synonym for the language defined aspect Type_Invariant
except
that it is separately controllable using pragma Assertion_Policy
.
3.25. Aspect Invariant’Class
This aspect is equivalent to pragma Type_Invariant_Class. It is a
synonym for the language defined aspect Type_Invariant'Class
except
that it is separately controllable using pragma Assertion_Policy
.
3.26. Aspect Iterable
This aspect provides a light-weight mechanism for loops and quantified
expressions over container types, without the overhead imposed by the tampering
checks of standard Ada 2012 iterators. The value of the aspect is an aggregate
with six named components, of which the last three are optional: First
,
Next
, Has_Element
, Element
, Last
, and Previous
.
When only the first three components are specified, only the
for .. in
form of iteration over cursors is available. When Element
is specified, both this form and the for .. of
form of iteration over
elements are available. If the last two components are specified, reverse
iterations over the container can be specified (analogous to what can be done
over predefined containers that support the Reverse_Iterator
interface).
The following is a typical example of use:
type List is private with
Iterable => (First => First_Cursor,
Next => Advance,
Has_Element => Cursor_Has_Element
[,Element => Get_Element]
[,Last => Last_Cursor]
[,Previous => Retreat]);
The values of
First
andLast
are primitive operations of the container type that return aCursor
, which must be a type declared in the container package or visible from it. For example:
function First_Cursor (Cont : Container) return Cursor;
function Last_Cursor (Cont : Container) return Cursor;
The values of
Next
andPrevious
are primitive operations of the container type that take both a container and a cursor and yield a cursor. For example:
function Advance (Cont : Container; Position : Cursor) return Cursor;
function Retreat (Cont : Container; Position : Cursor) return Cursor;
The value of
Has_Element
is a primitive operation of the container type that takes both a container and a cursor and yields a boolean. For example:
function Cursor_Has_Element (Cont : Container; Position : Cursor) return Boolean;
The value of
Element
is a primitive operation of the container type that takes both a container and a cursor and yields anElement_Type
, which must be a type declared in the container package or visible from it. For example:
function Get_Element (Cont : Container; Position : Cursor) return Element_Type;
This aspect is used in the GNAT-defined formal container packages.
3.27. Aspect Linker_Section
This aspect is equivalent to pragma Linker_Section.
3.28. Aspect Local_Restrictions
This aspect may be specified for a subprogram (and for other declarations as described below). It is used to specify that a particular subprogram does not violate one or more local restrictions, nor can it call a subprogram that is not subject to the same requirement. Positional aggregate syntax (with parentheses, not square brackets) may be used to specify more than one local restriction, as in
procedure Do_Something
with Local_Restrictions => (Some_Restriction, Another_Restriction);
Parentheses are currently required even in the case of specifying a single local restriction (this requirement may be relaxed in the future). Supported local restrictions currently include (only) No_Heap_Allocations and No_Secondary_Stack. No_Secondary_Stack corresponds to the GNAT-defined (global) restriction of the same name. No_Heap_Allocations corresponds to the conjunction of the Ada-defined restrictions No_Allocators and No_Implicit_Heap_Allocations.
Additional requirements are imposed in order to ensure that restriction violations cannot be achieved via overriding dispatching operations, calling through an access-to-subprogram value, calling a generic formal subprogram, or calling through a subprogram renaming. For a dispatching operation, an overrider must be subject to (at least) the same restrictions as the overridden inherited subprogram; similarly, the actual subprogram corresponding to a generic formal subprogram in an instantiation must be subject to (at least) the same restrictions as the formal subprogram. A call through an access-to-subprogram value is conservatively assumed to violate all local restrictions; tasking-related constructs (notably entry calls) are treated similarly. A renaming-as-body is treated like a subprogram body containing a call to the renamed subprogram.
The Local_Restrictions aspect can be specified for a package specification, in which case the aspect specification also applies to all eligible entities declared with the package. This includes types. Default initialization of an object of a given type is treated like a call to an implicitly-declared initialization subprogram. Such a “call” is subject to the same local restriction checks as any other call. If a type is subject to a local restriction, then any violations of that restriction within the default initialization expressions (if any) of the type are rejected. This may include “calls” to the default initialization subprograms of other types.
Local_Restrictions aspect specifications are additive (for example, in the case of a declaration that occurs within nested packages that each have a Local_Restrictions specification).
3.29. Aspect Lock_Free
This boolean aspect is equivalent to pragma Lock_Free.
3.30. Aspect Max_Queue_Length
This aspect is equivalent to pragma Max_Queue_Length.
3.31. Aspect No_Caching
This boolean aspect is equivalent to pragma No_Caching.
3.32. Aspect No_Elaboration_Code_All
This aspect is equivalent to pragma No_Elaboration_Code_All for a program unit.
3.33. Aspect No_Inline
This boolean aspect is equivalent to pragma No_Inline.
3.34. Aspect No_Tagged_Streams
This aspect is equivalent to pragma No_Tagged_Streams with an argument specifying a root tagged type (thus this aspect can only be applied to such a type).
3.35. Aspect No_Task_Parts
Applies to a type. If True, requires that the type and any descendants do not have any task parts. The rules for this aspect are the same as for the language-defined No_Controlled_Parts aspect (see RM-H.4.1), replacing “controlled” with “task”.
If No_Task_Parts is True for a type T, then the compiler can optimize away certain tasking-related code that would otherwise be needed for T’Class, because descendants of T might contain tasks.
3.36. Aspect Object_Size
This aspect is equivalent to attribute Object_Size.
3.37. Aspect Obsolescent
This aspect is equivalent to pragma Obsolescent. Note that the evaluation of this aspect happens at the point of occurrence, it is not delayed until the freeze point.
3.38. Aspect Part_Of
This aspect is equivalent to pragma Part_Of.
3.39. Aspect Persistent_BSS
This boolean aspect is equivalent to pragma Persistent_BSS.
3.40. Aspect Predicate
This aspect is equivalent to pragma Predicate. It is thus
similar to the language defined aspects Dynamic_Predicate
and Static_Predicate
except that whether the resulting
predicate is static or dynamic is controlled by the form of the
expression. It is also separately controllable using pragma
Assertion_Policy
.
3.41. Aspect Pure_Function
This boolean aspect is equivalent to pragma Pure_Function.
3.42. Aspect Refined_Depends
This aspect is equivalent to pragma Refined_Depends.
3.43. Aspect Refined_Global
This aspect is equivalent to pragma Refined_Global.
3.44. Aspect Refined_Post
This aspect is equivalent to pragma Refined_Post.
3.45. Aspect Refined_State
This aspect is equivalent to pragma Refined_State.
3.46. Aspect Relaxed_Initialization
For the syntax and semantics of this aspect, see the SPARK 2014 Reference Manual, section 6.10.
3.47. Aspect Remote_Access_Type
This aspect is equivalent to pragma Remote_Access_Type.
3.48. Aspect Secondary_Stack_Size
This aspect is equivalent to pragma Secondary_Stack_Size.
3.49. Aspect Scalar_Storage_Order
This aspect is equivalent to a attribute Scalar_Storage_Order.
3.51. Aspect Side_Effects
This aspect is equivalent to pragma Side_Effects.
3.52. Aspect Simple_Storage_Pool
This aspect is equivalent to attribute Simple_Storage_Pool.
3.53. Aspect Simple_Storage_Pool_Type
This boolean aspect is equivalent to pragma Simple_Storage_Pool_Type.
3.54. Aspect SPARK_Mode
This aspect is equivalent to pragma SPARK_Mode and may be specified for either or both of the specification and body of a subprogram or package.
3.55. Aspect Suppress_Debug_Info
This boolean aspect is equivalent to pragma Suppress_Debug_Info.
3.56. Aspect Suppress_Initialization
This boolean aspect is equivalent to pragma Suppress_Initialization.
3.57. Aspect Test_Case
This aspect is equivalent to pragma Test_Case.
3.58. Aspect Thread_Local_Storage
This boolean aspect is equivalent to pragma Thread_Local_Storage.
3.59. Aspect Universal_Aliasing
This boolean aspect is equivalent to pragma Universal_Aliasing.
3.60. Aspect Unmodified
This boolean aspect is equivalent to pragma Unmodified.
3.61. Aspect Unreferenced
This boolean aspect is equivalent to pragma Unreferenced.
When using the -gnat2022
switch, this aspect is also supported on formal
parameters, which is in particular the only form possible for expression
functions.
3.62. Aspect Unreferenced_Objects
This boolean aspect is equivalent to pragma Unreferenced_Objects.
3.63. Aspect User_Aspect
This aspect takes an argument that is the name of an aspect defined by a User_Aspect_Definition configuration pragma. A User_Aspect aspect specification is semantically equivalent to replicating the set of aspect specifications associated with the named pragma-defined aspect.
3.64. Aspect Value_Size
This aspect is equivalent to attribute Value_Size.
3.65. Aspect Volatile_Full_Access
This boolean aspect is equivalent to pragma Volatile_Full_Access.
3.66. Aspect Volatile_Function
This boolean aspect is equivalent to pragma Volatile_Function.
3.67. Aspect Warnings
This aspect is equivalent to the two argument form of pragma Warnings,
where the first argument is ON
or OFF
and the second argument
is the entity.