Version 1.1 of ai12s/ai12-0256-1.txt
!standard H.4.1(0) 18-01-31 AI12-0256-1/01
!class Amendment 18-01-31
!status work item 18-01-31
!status received 18-01-21
!subject Aspect No_Controlled_Subcomponents
Aspect No_Controlled_Subcomponents is added to Ada.
In high-integrity, embedded applications, it is usually necessary to
prove that the program will not run into stack overflow or other problems.
It is often required to prove these properties at the machine code level
with a special tool. The use of dynamic finalization greatly complicates
such analysis as it depends on implicit dynamic dispatching. Thus many such
applications ban finalization.
On the other hand, it is desirable, and becoming accepted, to use tagged
types and dynamic dispatching even in high-integrity applications.
Static analysis tools for stack usage can usually deal with the dynamic
dispatching (even if it introduces some over-estimation), but a harder
problem is that dynamic dispatching requires class-wide subtypes.
In general, class-wide subtypes are compiled such that any possible future
extension will work. That includes, of course, extensions that include
controlled components. This brings in finalization overhead, even if none of
the current types use any finalization.
It would be desirable to be able to declare that a type and any descendants
will not use any finalization, so this overhead can be eliminated (and thus,
eliminated from analysis).
[Editor's note: I'm not sure where this goes in the Standard. It seems
related to H.4, High-Integrity Restrictions, and it IS a restriction,
but only on a single type and its descendants. So I've put it there
H.4.1 Aspect No_Controlled_Subcomponents
Given a type T, the following type-related, operational aspects may be specified:
The type of this aspect is Boolean. If True, requires that the type and any
descendants do not have any controlled subcomponents. If specified, the
value of the expression shall be static. If not specified, the value of
this aspect is considered False.
The No_Controlled_Subcomponents aspect is nonoverridable (see 13.1.1).
AARM Note: This effectively requires that the aspect is specified (other than
as confirming) only on ultimate ancestor types that have no parent or
If No_Controlled_Subcomponents is True for a type, no component of the type
shall have a controlled subcomponent. In addition to the places where Legality
Rules normally apply (see 12.3), this rule also applies in the private part of
an instance of a generic unit.
When enforcing the above rule within a generic body, a generic formal private type
and a generic formal derived type of a composite type are considered to have a
AARM Reason: This is a typical generic assume-the-worst rule.
Modify 13.1.1(18.7/5) to include aspect No_Controlled_Subcomponents.
We could have extended this aspect to allow it to be given on generic formal
types. If specified True there, then only types with this aspect specified
True would match. This would allow declaring types with the aspect in a
generic body which have components of generic formal private types. However,
most such types can be declared in the private part of the generic (where
assume-the-best is used and a recheck is made if necessary). So this was
The only Ada 2012 way to eliminate finalization is to use pragma
Restrictions (No_Dependence => Ada.Finalization); However, this requires the
entire program (including the runtime) to avoid using finalization. This means
that features like storage pools and the bounded indefinite container(s) [see
AI12-0254-1] cannot be used in such programs, even if they are designed with
trivial finalization. (Most compilers can eliminate finalization overhead from
objects with trivial finalization.)
The proposed aspect allows eliminating overhead specifically from class-wide
type hierarchies while still allowing controlled types to appear in the runtime
[Not sure. Not sure how aspects are handled - Editor.]
ACATS B- and C-Tests are needed to check that the new capabilities are
This AI was split from AI12-0254-1. The original request for this aspect
can be found in the !appendix of that AI, in a message dated Sunday, January
21, 2018, 9:48 AM.
Questions? Ask the ACAA Technical Agent