From: Robert A Duff <bobduff@world.std.com>
Subject: Re: Operator visibility question
Date: Sun, 3 Jun 2001 20:13:52 GMT
Date: 2001-06-03T20:13:52+00:00 [thread overview]
Message-ID: <wccbso5fhj3.fsf@world.std.com> (raw)
In-Reply-To: ba18d5cb.0106030548.62aa45e2@posting.google.com
rod@praxis-cs.co.uk (Rod Chapman) writes:
> Can anyone please tell me if the following code is legal?
In what language -- Ada or SPARK? ;-) ;-)
> package MT
> is
> type T is range 0 .. 4;
> end MT;
>
> with MT;
> --# inherit MT;
> package VT
> is
> function "+" (Left, Right : in MT.T) return MT.T renames MT."+";
> A : constant := 2;
> B : constant MT.T := 3;
>
> C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
There are several "<" operators directly visible here, including the one
for root_integer. But none of them apply -- the "<" for MT.T is not
directly visible here. So I believe this is illegal in Ada, unless I'm
missing something.
A and 2 are both of type universal_integer, and there are implicit
conversions from u_i to any integer type, but there is no implicit
conversion from MT.T to root_real.
Sounds like a GNAT bug. Seems like SPARK is correct here.
> end VT;
>
> The SPARK Examiner rejects the declaration of C with the message:
>
> 9 C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
> ^
> *** Semantic Error :309: Operator not visible for these types.
>
> On the other hand, GNAT 3.13 accepts the code with no errors. Can anyone
> explain which is right, and (more importantly) why?
> Cheers,
> Rod Chapman
> SPARK Team
> Praxis Critical Systems
prev parent reply other threads:[~2001-06-03 20:13 UTC|newest]
Thread overview: 12+ messages / expand[flat|nested] mbox.gz Atom feed top
2001-06-03 13:48 Operator visibility question Rod Chapman
2001-06-03 14:19 ` Jeff Creem
2001-06-03 15:47 ` Nacho Robledo
2001-06-03 20:15 ` Robert A Duff
2001-06-04 15:24 ` Rod Chapman
2001-06-04 17:55 ` Nacho Robledo
2001-06-04 21:27 ` Ted Dennison
2001-06-03 16:34 ` Florian Weimer
2001-06-04 15:52 ` Ted Dennison
2001-06-04 22:12 ` Florian Weimer
2001-06-05 12:24 ` Rod Chapman
2001-06-03 20:13 ` Robert A Duff [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox