Version 1.1 of ai12s/ai12-0338-1.txt
!standard 7.3.2(18.1/5) 19-06-15 AI12-0338-1/01
!class binding interpretation 19-06-15
!status work item 19-06-15
!status received 19-06-14
!priority Low
!difficulty Easy
!qualifier Omission
!subject type invariant checking and incomplete types
!summary
Type invariants for type T are not checked for incomplete types whose
completion is not available, even if that completion has components of type T.
!question
In the rules about when type invariants are checked, one case is:
an access-to-object parameter or result whose designated nominal type
has a part of type T;
What does this mean when the designated nominal type is incomplete? (There is
no check.)
For example:
limited with P2;
package P1 is
type T1 is private with
Type_Invariant => Is_Ok (T1);
function Is_Ok (X : T1) return Boolean;
procedure Op (T2_Ref : access P2.T2);
private
type T1 is new Integer;
function Is_Ok (X : T1) return Boolean is (X mod 123 /= 45);
end P1;
with P1.Child;
package body P1 is
procedure Op (T2_Ref : access P2.T2) is
begin
P1.Child.Child_Op (T2_Ref);
end Op;
end P1;
private package P1.Child is
procedure Child_Op (T2_Ref : access P2.T2);
end P1.Child;
with P2;
package body P1.Child is
procedure Child_Op (T2_Ref : access P2.T2) is
begin
T2_Ref.all := (123, 45);
end Child_Op;
end P1.Child;
with P1;
package P2 is
type T2 is array (Boolean) of P1.T1;
end P2;
with P1, P2;
procedure Main is
Ptr : access P2.T2 := new P2.T2;
begin
P1.Op (Ptr);
end Main;
!recommendation
(See Summary.)
!wording
Replace 7.3.2(18.1/5):
an access-to-object parameter or result whose designated nominal type
has a part of type T;
with:
an access-to-object parameter or result whose designated nominal type
has a part of type T and either the designated nominal type is not an
incomplete view (at the point of the declaration of the callable
entity) or the completion of the designated nominal type occurs in
the same declaration list as the incomplete declaration.
AARM note: This ensures that the completion of the designated nominal
type is available when determining the parts that need to be checked.
Modify AARM 7.3.2(23.a/5):
... is not itself externally visible. { Incomplete types or
class-wide types may be used to produce cases where subcomponents
are not checked. } These cases represent holes ...
!discussion
To the extent that this obscure corner case has any importance at all, a check
failure would be preferable from the user's perspective because it prevents a
"bad" value from leaking out.
This interpretation is also consistent with the AI12-0191 rule:
For example, a reference to the components of an object in a
rule that is interpreted at compile-time would not apply to
components that are not visible. On the other hand, a reference
to the components of an object in a dynamic semantics rule would
apply to all components of the object, visible or not, including
(for tagged objects) components which are not components of the
nominal type of the object (see 3.9.1). Other terms, such as
"subcomponent" and "part", are interpreted analogously.
But this could be burdensome for implementations because it could require
checking the values of subcomponents whose existence is unknown at the point
where invariant checking code is being generated.
If, for example, the implementation chooses to generate invariant checking code
as part of code generation for the body of the callee (which is a reasonable
choice that we don't want to preclude), then the completion of the designated
type is unavailable and heroic measures would be required to generate a type
invariant check.
!ASIS
No ASIS effect.
!ACATS test
An ACATS C-Test should be constructed for a case like this.
!appendix
From: Steve Baird
Sent: Saturday, June 15, 2019 3:58 PM
Opening a new AI, spun off from AI12-0191. [This is version /01 of the
AI - Editor.]
****************************************************************
Questions? Ask the ACAA Technical Agent