!standard 6.5(5.2/2)                                      08-08-14  AI05-0103-1/03
!class binding interpretation 08-06-15
!status work item 08-06-15
!status received 06-04-25
!priority Low
!difficulty Medium
!qualifier Omission
!subject Return statements should require at least static compatibility

!summary

The subtype_indication in an extended_return_statement must be statically
compatible with the result subtype of the function, and for elementary
types, must statically match the result type.

!question

We use static matching to require that null exclusions match on a function
and any extended return:

    type An_Access is access Integer;

    function Nice return not null An_Access is
    begin
        return Obj : An_Access do -- ERROR:
            Obj := null;
        end return;
    end Nice;

This is because 6.5(5.2/2) requires static matching for the
subtype_indication and the result subtype if the result subtype is
constrained. An_Access is constrained as defined by 3.10(14/1).

But consider the following small change to An_Access:

    type An_Access is access String;

    function Nice return not null An_Access is
    begin
        return Obj : An_Access do -- OK!!
            Obj := null;
        end return;
    end Nice;

Now An_Access is not constrained as defined by 3.10(14/1) [the designated
subtype is an unconstrained array]. Thus the first part of 6.5(5.2/2) does
not apply, and no matching is required. So it appears that we've succeeded
in returning null from a null-excluding function. Ouch.

!wording

Modify 6.5(5.2) (as previous modified by AI05-0032-1):

If the result subtype of the function is defined by a subtype_mark, the
return_subtype_indication shall be a subtype_indication. The type of the
subtype_indication shall be covered by the result type of the function.
[If the result subtype of the function is constrained, then the]{The} subtype
defined by the subtype_indication shall [also ]be {statically compatible
with the result subtype of the function; if the result type of the function
is elementary, the two subtypes }[constrained and ]shall statically
match[ this result subtype]. If the result subtype of the function is
[unconstrained]{indefinite}, then the subtype defined
by the subtype_indication shall be a definite subtype, or there shall be an
expression.

!discussion

This new wording correctly handles the cases involving null exclusions
because these are handled correctly in the definition of static compatibility.
The new wording does not need to talk about "constrained" and "unconstrained"
as that is included in the definition of static compatibility.

The existing stricter checking for elementary types is preserved; this
disallows the following (arguably reasonable) example:

   function F1 return Integer is
   begin
     return X : Natural do -- illegal
       ...;
     end return;
   end F1;

Recall that static compatibility of constrained scalar types does not
imply static matching as it does for other constrained types.
There would be no definitional problems associated with omitting
   "; if the result type of the function is elementary, then
    the two subtypes shall statically match"
from the wording above, but there does not seem to be adequate
justification for changing the language to allow cases such
as the preceding example.

[Editor's note: This also makes access constraints illegal. For example:
   function F2 return Acc_String is
   begin
     return X : Acc_String(1..10) do -- illegal
       ...
     end return;
   end F2;
Unlike composite types, this constraint is not needed nor used to determine
the shape of the designated object. That comes from the allocator that created
it (or, in the case of 'Access, the aliased object itself). So no capability
is lost by this restriction. The extra checks that would be needed to 
implement this constraint buy little, especially as they are not required
by the specification of the function.]


Is "static compatibility" well defined in the case where the the
type of the first subtype is covered by, but is not the same as,
the type of the second subtype? Pending the resolution of AI05-0057, all
we really depend on is a rule that if T is the first named subtype of a
specific tagged type, then any subtype of any type that is covered by T
is statically compatible with T'Class. If that is not the case (e.g.,
if it were determined that static compatibility is only defined for two
subtypes of the same type), then further wording changes are needed.

--!corrigendum 6.5(5.2/2)

!ACATS Test


!appendix

From: Randy Brukardt
Sent: Friday, April 25, 2008  12:06 AM

Here's another one that will remind you that I'm working on ACATS tests...

We use static matching to require that null exclusions match on a function
and any extended return:

    type An_Access is access Integer;

    function Nice return not null An_Access is
    begin
        return Obj : An_Access do -- ERROR:
            Obj := null;
        end return;
    end Nice;

This is because 6.5(5.2/2) requires static matching for the
subtype_indication and the result subtype if the result subtype is
constrained. An_Access is constrained as defined by 3.10(14/1).

But consider the following small change to An_Access:

    type An_Access is access String;

    function Nice return not null An_Access is
    begin
        return Obj : An_Access do -- OK!!
            Obj := null;
        end return;
    end Nice;

Now An_Access is not constrained as defined by 3.10(14/1) [the designated
subtype is an unconstrained array]. Thus the first part of 6.5(5.2/2) does
not apply, and no matching is required. So it appears that we've succeeded
in returning null from a null-excluding function. That surely won't do.

Luckily, Tucker has already filled the hole: AI05-0032-1 adds "A check
is made that the value of the return object belongs to the function
result subtype.", and that clearly will fail. So at least Constraint_Error
will be raised. (Before AI05-0032-1, we would have had to return null,
as there was no check. Lovely.)

However, it is annoying that we've lost a compile-time check for a reason
that is completely unrelated to the check itself. It also means that
AARM note 6.5(5.g/3) is a lie.

Obviously, fixing the AARM note is easy; this case should be mentioned in
the AARM. But should we tweak the rules to ensure that null exclusion
checks are always made even if the access type is unconstrained (we don't
care about that for this purpose - null exclusions aren't a constraint
anyway)? In that case, the AARM note is fine (and there isn't going
to be a nasty ACATS test...)

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

From: Robert A. Duff
Sent: Friday, April 25, 2008  7:50 AM

> Obviously, fixing the AARM note is easy; this case should be mentioned 
> in the AARM. But should we tweak the rules to ensure that null 
> exclusion checks are always made even if the access type is unconstrained ...

Yes.

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