type casting tagged types in the wrong direction

type casting tagged types in the wrong direction

[James A. Squire]

I have a question:

Say I have something like:

type A is tagged
  record
    X : ABC;
    Y : DEF;
  end record;

type B is new A with
  record
    W : GHI;
  end record;

type C is new B with
  record
    Z : JKL;
  end record;


OK.  Now, let's say that I forgot which type extends off of which, and I
write a statement like this:

  Jim  : C;
  Jane : B;
  Save : JKL;

begin
  ...
  Jim := C (Jane);
  Save := Jim.Z;
  ...
end;

GNAT 3.03 compiles this statement.  Is that really right?  Is Jim.Z
defined?
According to the LRM 4.6, the above is called a "view conversion".  This
raises the question, how do you take a type C view of a type B entity
when type C looks for additional information?

Should a validated Ada95 compiler flag this usage?  I realize that GNAT
is not validated.

I would appreciate any expert or otherwise opinions that any of you have
to offer.
Thank you.
--
James Squire
MDA Avionics Tools & Processes
ja_squire@csehp3.mdc.com
"one of these days I'm going to better myself by going to Knight school"

Re: type casting tagged types in the wrong direction

[Norman H. Cohen]

In article <3159B860.28A6@csehp3.mdc.com>, "James A. Squire"
<m193884@CSEHP3.MDC.COM> writes: 

|> Say I have something like: 
|>
|> type A is tagged
|>   record
|>     X : ABC;
|>     Y : DEF;
|>   end record;
|>
|> type B is new A with
|>   record
|>     W : GHI;
|>   end record;
|>
|> type C is new B with
|>   record
|>     Z : JKL;
|>   end record;
|>
|>
|> OK.  Now, let's say that I forgot which type extends off of which, and I
|> write a statement like this: 
|>
|>   Jim  : C;
|>   Jane : B;
|>   Save : JKL;
|>
|> begin
|>   ...
|>   Jim := C (Jane);
|>   Save := Jim.Z;
|>   ...
|> end;
|>
|> GNAT 3.03 compiles this statement.  Is that really right?  Is Jim.Z
|> defined?

The expression Jim.Z is perfectly legal, but the type conversion C(Jane)
is not.  This should be flagged as a compile-time error, because it does
not satisfy the conditions in either 4.6(22) or 4.6(23).

--
Norman H. Cohen    ncohen@watson.ibm.com

Re: type casting tagged types in the wrong direction

[Tucker Taft]

James A. Squire (m193884@CSEHP3.MDC.COM) wrote:
: I have a question:

: Say I have something like:

: type A is tagged
:   record
:     X : ABC;
:     Y : DEF;
:   end record;

: type B is new A with
:   record
:     W : GHI;
:   end record;

: type C is new B with
:   record
:     Z : JKL;
:   end record;


: OK.  Now, let's say that I forgot which type extends off of which, and I
: write a statement like this:

:   Jim  : C;
:   Jane : B;
:   Save : JKL;

: begin
:   ...
:   Jim := C (Jane);

This is illegal, by RM95 4.6(21-23).

:   Save := Jim.Z;
:   ...
: end;

: GNAT 3.03 compiles this statement.  Is that really right?  

No.  GNAT should have complained at compile time about the conversion
from B to C.  You may convert from B'Class to C (and then a run-time
check is performed), or you may convert from C to B, but a direct
conversion from B to C is illegal.

: ... Is Jim.Z defined?

Jim.Z is "defined," but the conversion on the previous line
is illegal, so who knows what code GNAT is generating for the
assignment to Jim.

: According to the LRM 4.6, the above is called a "view conversion".  This
: raises the question, how do you take a type C view of a type B entity
: when type C looks for additional information?

You can't.

: Should a validated Ada95 compiler flag this usage?  I realize that GNAT
: is not validated.

GNAT is validated, but validation doesn't guarantee bug-free
(nor does anything else I know of ;-).

This looks like a bug in GNAT, pure and simple.  (It also *suggests*
that another ACVC test might be in order ;-).

: I would appreciate any expert or otherwise opinions that any of you have
: to offer.
: Thank you.
: --
: James Squire
: MDA Avionics Tools & Processes
: ja_squire@csehp3.mdc.com
: "one of these days I'm going to better myself by going to Knight school"

-Tucker Taft   stt@inmet.com   http://www.inmet.com/~stt/
Intermetrics, Inc.  Cambridge, MA  USA

Re: type casting tagged types in the wrong direction

[Robert Dewar]

Norman said:

"The expression Jim.Z is perfectly legal, but the type conversion C(Jane)
is not.  This should be flagged as a compile-time error, because it does
not satisfy the conditions in either 4.6(22) or 4.6(23)."

GNAT certainly agrees:

    28.   Jim := C (Jane);
                    |
        >>> downward conversion of tagged objects not allowed

:-)

Re: type casting tagged types in the wrong direction

[Robert Dewar]

Jon said

": Should a validated Ada95 compiler flag this usage?  I realize that GNAT
: is not validated."

You realize wrong! GNAT was the first general purpose Ada 95 compiler
to be validated. We validated on the floor at Tri-Ada 96, and are now
the proud owners of ACVC 2.0 validation certificates numbers 2, 3 and
4. These validations were for SGI machines, but we expect many othr
GNAT validations in the future.

Of course validation does not ensure 100% compliance, so it is by no
means amazing to find a bug, but in fact this particular bug is
certainly fixed now (I don't know when exactly it was fixed), and
we now get a nice error message.

Re: type casting tagged types in the wrong

[Scott Moody]

I run this same program with GNAT 3.03 on solaris
and it reports the error correctly:

tmp.adb:24:14: downward conversion of tagged objects not allowed
gnatmake: *** compilation failed.


----source:
procedure tmp is

 type A is tagged
   record
     X : integer;
     Y : integer;
   end record;

 type B is new A with
   record
     W : integer;
   end record;

 type C is new B with
   record
     Z : integer;
   end record;

   Jim  : C;
   Jane : B;
   Save : integer;

 begin
   Jim := C (Jane);
   Save := Jim.Z;
 end;

Re: type casting tagged types in the wrong direction

[Robert Dewar]

So the one at ftp://cs.nyu.edu/pub/gnat/ is validated?  The ones you
mention above are commercially available from SGI.

  The validation of GNAT was carried out by Ada Core Technologies, and
  the validation certificates are jointly held by SGI and ACT. I believe
  the validated version is not yet actually available from SGI (it is
  in beta test now), but it is available from us. Not by FTP from some
  public site we have no control over (who knows what bits you are getting
  there, we cannot take formal responsibility for versions of GNAT you get
  from some public FTP directory). However, we can definitely supply you
  with an officially validated version today for the SGI if you want one.

  A bug like this is undoubtedly host/target independent, so it is
  undoubtedly present in the validated version.


Perhaps I am a virgin, but I don't see how a compiler passes validation
without properly giving an error message.  Tucker Taft mentioned
something about needing a new ACVC test.  Sounds to me like the
validation suite ain't quite up to snuff yet.  Of course, that's true
anyway since there is no such thing yet as full validation anyway.
There won't be until a year from now (ACVC 2.1 is what is needed for
full validation).

  If you think that ANY testing guarantees 100% freedom from all bugs,
  you are indeed a virgin! No test suite can possibly make this guarantee.
  Even if the number of tests were multiplied by 100, there could still
  be errors, and indeed compilers are pretty complex programs, and
  ensuring that a compiler for a language like C++ or Ada is 100%
  error free is beyond the state of the art.

  What Tuck suggested is that this particular error seems like something
  that should be checked by the ACVC suite. This is true, and in fact
  2.1 contains such a test, but note again that if you think that "full
  validation" means that all possible tests are present, you are much
  mistaken.


What do you mean by "now"?  It is not fixed in 3.03 (which is what I am
running), and according to the above mentioned ftp site this is still
the latest version, so it is most certainly not fixed "now".

  I mean that it is fixed in version 3.04, which is already being run by
  some of our customers. Version 3.04 will be publically released some
  time in the future. I don't know when this bug was fixed -- a while
  ago it seems, but it is certainly possible that one or more versions
  of 3.03 may exhibit this bug.

Re: type casting tagged types in the wrong direction

[James A. Squire]

Robert Dewar <dewar@CS.NYU.EDU> wrote:

> You realize wrong! GNAT was the first general purpose Ada 95 compiler
> to be validated. We validated on the floor at Tri-Ada 96, and are now
> the proud owners of ACVC 2.0 validation certificates numbers 2, 3 and
> 4. These validations were for SGI machines, but we expect many othr
> GNAT validations in the future.

So the one at ftp://cs.nyu.edu/pub/gnat/ is validated?  The ones you
mention above are commercially available from SGI.

> Of course validation does not ensure 100% compliance, so it is by no

Perhaps I am a virgin, but I don't see how a compiler passes validation
without properly giving an error message.  Tucker Taft mentioned
something about needing a new ACVC test.  Sounds to me like the
validation suite ain't quite up to snuff yet.  Of course, that's true
anyway since there is no such thing yet as full validation anyway.
There won't be until a year from now (ACVC 2.1 is what is needed for
full validation).

> means amazing to find a bug, but in fact this particular bug is
> certainly fixed now (I don't know when exactly it was fixed), and
> we now get a nice error message.

What do you mean by "now"?  It is not fixed in 3.03 (which is what I am
running), and according to the above mentioned ftp site this is still
the latest version, so it is most certainly not fixed "now".
--
James Squire
MDA Avionics Tools & Processes
ja_squire@csehp3.mdc.com
"one of these days I'm going to better myself by going to Knight school"

Re: type casting tagged types in the wrong direction

[Fergus Henderson]

dewar@cs.nyu.edu (Robert Dewar) writes:

>You realize wrong! GNAT was the first general purpose Ada 95 compiler
>to be validated. We validated on the floor at Tri-Ada 96, and are now
>the proud owners of ACVC 2.0 validation certificates numbers 2, 3 and
>4.

So who got validation certificate number 1?

--
Fergus Henderson             	WWW: http://www.cs.mu.oz.au/~fjh
fjh@cs.mu.oz.au              	PGP: finger fjh@128.250.37.3

Re: type casting tagged types in the wrong direction

[Robert Dewar]

"
So who got validation certificate number 1?"

Intermetrics, for the Patriot 2 compiler. But I don't think that
qualifies as a generl purpose compiler -- not too many people have
a Patriot 2 nosecone sitting on their desks.

Actually several validations happened pretty close. Intermetrics was
a couple of weeks before Tri-Ada, GNAT validated at Tri-Ada, and
Thompson validated a couple of weeks after Tri-Ada (the latter
compiler of course also quaifies as general purpose!)