Version 1.2 of ai22s/ai22-0014-1.txt

Unformatted version of ai22s/ai22-0014-1.txt version 1.2
Other versions for file ai22s/ai22-0014-1.txt

!standard 3.4(27/2)          22-02-03 AI22-0014-1/02
!class binding interpretation 21-11-12
!status Corrigendum 1-2022 22-02-03
!status ARG Approved 15-0-1 22-02-03
!status work item 21-11-12
!status received 21-09-09
!priority Low
!difficulty Easy
!qualifier Omission
!subject Predicates on inherited functions
!summary
It should be clarified that a predicate check is performed on the result returned by a function with a controlling result that is inherited by a null extension, if there is a predicate on the null extension.
!issue
In the following example:
procedure Inherited is package P1 is type T1 is tagged record X : Integer; end record; function F return T1; V : constant T1 := (X => 0); end P1; package P2 is type T2 is new P1.T1 with null record with Dynamic_Predicate => X > 0; V : constant T2 := (X => 1); end P2; package body P1 is function F return T1 is (V); end P1; procedure Bad is begin pragma Assert (P1.T1'Class (P2.F).X = 0); -- Should fail a predicate check. end Bad; begin Bad; end Inherited;
P1.T1 is a tagged type and P2.T2 is derived from T1 with a null extension and a subtype predicate. The primitive function F of T1 is inherited by T2. The question is, should there be a predicate check when calling P2.F? (Yes.)
!recommendation
There should be a predicate check when calling P2.F in the above, because if we were to write the overriding manually, there would be one.
!wording
Modify 3.4(27/2) as follows:
... If the result type of the inherited subprogram is the derived type, the result of calling the subprogram of the parent or progenitor is converted to the derived type, or in the case of a null extension, extended to the derived type using the equivalent of an extension_aggregate with the original result as the ancestor_part and null record as the record_component_association_list. {In either case, the result is then converted to the corresponding subtype [Redundant:(as defined above)] of the derived type.}
!discussion
It was unclear whether a predicate check is mandated by the RM in the example given in the !question, as no predicate checks occur on aggregates and it is not said that the result of the call is converted to the derived (sub)type.
In an earlier paragraph in the same section (3.4(19)), "corresponding subtype" is defined to be the first subtype in the case of a record extension (and hence also a null extension), and in the example, the first subtype of the derived type has a dynamic predicate. So by clarifying that the conversion to the corresponding subtype occurs, the appropriate check would be performed.
!corrigendum 3.4(27/2)
Replace the paragraph:
For the execution of a call on an inherited subprogram, a call on the corresponding primitive subprogram of the parent or progenitor type is performed; the normal conversion of each actual parameter to the subtype of the corresponding formal parameter (see 6.4.1) performs any necessary type conversion as well. If the result type of the inherited subprogram is the derived type, the result of calling the subprogram of the parent or progenitor is converted to the derived type, or in the case of a null extension, extended to the derived type using the equivalent of an extension_aggregate with the original result as the ancestor_part and null record as the record_component_association_list.
by:
For the execution of a call on an inherited subprogram, a call on the corresponding primitive subprogram of the parent or progenitor type is performed; the normal conversion of each actual parameter to the subtype of the corresponding formal parameter (see 6.4.1) performs any necessary type conversion as well. If the result type of the inherited subprogram is the derived type, the result of calling the subprogram of the parent or progenitor is converted to the derived type, or in the case of a null extension, extended to the derived type using the equivalent of an extension_aggregate with the original result as the ancestor_part and null record as the record_component_association_list. In either case, the result is then converted to the corresponding subtype (as defined above) of the derived type.
!ACATS test
An ACATS C-Test should be constructed to check that the runtime predicate check is made.
!appendix

From: Claire Dross
Sent: Thursday, September 9, 2021  9:14 AM

Hi all,

We have come up recently with the following example:

procedure Inherited with SPARK_Mode is
   package P1 is
      type T1 is tagged record
         X : Integer;
      end record;
      function F return T1;
      V : constant T1 := (X => 0);
   end P1;
   package P2 is
      type T2 is new P1.T1 with null record with Predicate => X > 0;
      V : constant T2 := (X => 1);
   end P2;
   package body P1 is
      function F return T1 is (V);
   end P1;
   procedure Bad is
   begin
      pragma Assert (P1.T1'Class (P2.F).X = 0); --@PREDICATE_CHECK:FAIL
   end Bad;
begin
   Bad;
end Inherited;

P1.T1 is a tagged type and P2.T2 is derived from T1 with a null extension 
and a subtype predicate. The primitive function F of T1 is inherited by T2.
The question is, should there be a predicate check when calling P2.F? I 
personally think there should be one, because if we were to write the 
overriding manually, there would be one. However it is unclear whether such
a check is mandated by the RM as no predicate checks occur on aggregates and
it is not said that the result of the call is converted to the derived type.
What do others think?

****************************************************************

From: Tucker Taft
Sent: Thursday, September 9, 2021  12:13 PM

I agree that the wording in 3.4(27/2) should be augmented, perhaps as follows:

... If the result type of the inherited subprogram is the derived type, the 
result of calling the subprogram of the parent or progenitor is converted to
the derived type, or in the case of a null extension, extended to the derived
type using the equivalent of an extension_aggregate with the original result
as the ancestor_part and null record as the record_component_association_list.
{In either case, the result is then converted to the corresponding subtype 
[Redundant:(as defined above)] of the derived type.}

In an earlier paragraph in the same section (3.4(19)), "corresponding subtype" 
is defined to be the first subtype in the case of a record extension (and hence
also a null extension), and in the example, the first subtype of the derived
type has a dynamic predicate.  (The example uses the GNAT-specific Predicate 
aspect, which automatically selects Dynamic_Predicate or Static_Predicate.)
So by clarifying that the conversion to the corresponding subtype occurs, the
appropriate check would be performed.

****************************************************************

Questions? Ask the ACAA Technical Agent