H.7 Extensions to Global and Global'Class Aspects
This Reference Manual output has not been verified, and may contain omissions or errors. Report any problems on the tracking issue
In addition to the entities specified in 6.1.2, the Global aspect may be specified for a subtype (including a formal subtype), formal package, formal subprogram, and formal object of an anonymous access-to-subprogram type.
The following additional syntax is provided to override the mode of a formal parameter to reflect indirect effects on variables reachable from the formal parameter by one or more access-value dereferences:
Name Resolution Rules4/5
name that is associated with an overriding mode shall resolve to statically denote a formal object, or a formal parameter of the associated entity.
The presence of the reserved word overriding in a global mode indicates that the specification is overriding the mode of a formal parameter with another mode to reflect the overall effect of an invocation of the callable entity on the state associated with the corresponding actual parameter.
[As described in 6.1.2, the following rules are defined in terms of operations that are performed by or on behalf of an entity.]
The Global aspect for a subtype identifies the global variables that can be referenced during default initialization, adjustment as part of assignment, finalization of an object of the subtype, or conversion to the subtype, including the evaluation of any assertion expressions that apply. If not specified for the first subtype of a derived type, the aspect defaults to that of the ancestor subtype; if not specified for a nonderived composite first subtype the aspect defaults to that of the enclosing library unit; if not specified for a nonderived elementary first subtype (or scalar base subtype), the aspect defaults to null in the absence of a predicate (or when the predicate is statically True), and to that of the enclosing library unit otherwise. If not specified for a nonfirst subtype S, the Global aspect defaults to that of the subtype identified in the
subtype_indication defining S.
The Global'Class aspect may be specified for the first subtype of a tagged type T, indicating an upper bound on the Global aspect of any descendant of T. If not specified, it defaults to Unspecified.
For a tagged subtype T, each mode of its Global aspect shall identify a subset of the variables identified either by the corresponding mode, or by the in out mode, of the Global'Class aspect of the first subtype of any ancestor of T.
Extensions to Ada 2012
H.7.1 The Use_Formal and Dispatching Aspects1/5
The Use_Formal and Dispatching aspects are provided to more precisely describe the use of generic formal parameters and dispatching calls within the execution of an operation, enabling more precise checking of conformance with the Nonblocking and global aspects that apply at the point of invocation of the operation.
For any declaration within a generic unit for which a global or Nonblocking aspect may be specified, other than a
generic_formal_parameter_declaration, the following aspect may be specified to indicate which generic formal parameters are used by the associated entity:
- The aspect is specified with a
formal_parameter_set, with the following form:
::=null | all 6/5
For any declaration for which a global or Nonblocking aspect may be specified, other than for a library package, a generic library package, or a generic formal, the following aspect may be specified:
- The aspect is specified with a
dispatching_operation_set, with the following form:
Name Resolution Rules11/5
formal_parameter_name in a Use_Formal aspect shall resolve to statically denote a formal subtype, a formal subprogram, or a formal object of an anonymous access-to-subprogram type[ of an enclosing generic unit or visible formal package].
name of a
dispatching_operation_specifier shall resolve to statically name an object (including possibly a formal parameter) of a tagged class-wide type T'Class, or of an access type designating a tagged class-wide type T'Class; the dispatching_operation_
name of the
dispatching_operation_specifier shall resolve to statically denote a dispatching operation associated with T.
The formal parameter set is identified by a set of
formal_parameter_names. Alternatively, the reserved word null may be used to indicate none of the generic formal parameters, or all to indicate all of the generic formal parameters, of any enclosing generic unit (or visible formal package) can be used within the execution of the operation. If there is no formal parameter set specified for an entity declared within a generic unit, it defaults to all.
The dispatching operation set is identified by a set of
dispatching_operation_specifiers. It indicates that the Nonblocking and global effects of dispatching calls that match one of the specifiers, rather than being accounted for by the Nonblocking or global aspect, are instead to be accounted for by the invoker of the operation. A dispatching call matches a
dispatching_operation_specifier if the
prefix of the call statically denotes the same operation(s) as that of the
dispatching_operation_specifier, and at least one of the objects controlling the call is denoted by, or designated by, a
name that statically names the same object as that denoted by the object_
name of the
In the absence of any
dispatching_operation_specifiers, or if none of them match a dispatching call C within an operation P, Nonblocking and global aspects checks are performed at the point of the call C within P using the Nonblocking and Global'Class aspects that apply to the dispatching operation named in call C. If there is a match, any global access or potential blocking within the subprogram body invoked by the call C is ignored at the point of call within P. Instead, when the operation P itself is invoked, Nonblocking and global aspect checks are performed presuming each named dispatching operation is called at least once (with the named object controlling the call), but similarly ignoring those dispatching calls that would match a
dispatching_operation_specifier applicable at the point of invocation of P.
Within an operation to which a Use_Formal aspect applies, if the formal parameter set is anything but all, then the only generic formal subtypes that may be used, the only formal subprograms that may be called, and the only formal objects of an anonymous access-to-subprogram type that may be dereferenced as part of a call or passed as the actual for an access parameter, are those included in the formal parameter set.
When an operation (or instance thereof) to which a Use_Formal aspect applies is invoked, Nonblocking and global aspect checks are performed presuming each generic formal parameter (or corresponding actual parameter) of the formal parameter set is used at least once.
An example of use of the Dispatching aspect:
procedure My_Write( -- see 13.13.2 Stream : not null access Ada.Streams.Root_Stream_Type'Class; Item : My_Integer'Base) with Dispatching => Write(Stream); for My_Integer'Write use My_Write;
For examples of use of the Use_Formal aspect, see the Element functions of Hashed_Sets in A.18.8.