Re: GNAT GPL 2013 bug?

[Adam Beneschan <adambeneschan@aol.com>]

On Friday, August 9, 2013 11:39:19 AM UTC-7, Adam Beneschan wrote:

> >    package Dmitry is
> >       type Q is private;
> >       procedure P (X : access Q) is null;
> >    private
> >       type Q is tagged null record;
> >    end Dmitry;
> 
> >    with Dmitry; use Dmitry;
> >    procedure Test_Dmitry is
> >       Y : access Q;
> >    begin
> >       P (Y);                  ------ dmitry.ada:11
> >    end Test_Dmitry;

> > gcc -c -gnat12 test_dmitry.adb
> > dmitry.ada:9:04: warning: variable "Y" is read but never assigned
> > dmitry.ada:11:07: warning: null value not allowed here
> > dmitry.ada:11:07: warning: "Constraint_Error" will be raised at run time

> Offhand, I do think GNAT is wrong, and that P is not a dispatching procedure.  However, the language rules get a bit murky at times when untagged private types are completed with tagged types, and sometimes the rules have had to be changed because they didn't cover this case adequately.  I'll have to dig a bit further.

OK, it turns out GNAT is right; AI95-183 says that P is dispatching.  I don't particularly like that, since it seems to make the behavior, from the caller's point of view, dependent on what's in the private part that the caller isn't supposed to have to know about.  It was probably OK, though, if the only effect was that a call to P might actually call some other P in some other package.  However, now that the "not null" rules on anonymous access parameters have changed, I think this *is* a problem, since now you can't tell whether a null value is allowed for the access parameter without peeking into the private part.  (I think AI95-183 was answered before the "not null" feature was proposed.)  So there seems to be a privacy breakage here.

A possible solution: Add a rule that if an untagged private type has a full definition that is tagged, then in any primitive operations declared in the visible part with controlling access parameters, the access parameters must be declared with *explicit* null exclusions.  This means that the example suggested by Dmitry and Simon would be caught early--the package specification would be disallowed.  This wouldn't be backward-compatible.  I'm guessing that in practice, this might require modifications to approximately zero code.  

                             -- Adam