From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: border1.nntp.dca.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!eu.feeder.erje.net!gandalf.srv.welterde.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Class Wide Type Invariants - My bug or compiler bug Date: Wed, 26 Feb 2014 19:01:45 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <3b16296c-3a9b-478e-a113-44415f665121@googlegroups.com> <3cf20663-960d-4ab1-9210-08042ca6af43@googlegroups.com> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1393462905 20899 69.95.181.76 (27 Feb 2014 01:01:45 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 27 Feb 2014 01:01:45 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: number.nntp.dca.giganews.com comp.lang.ada:185090 Date: 2014-02-26T19:01:45-06:00 List-Id: wrote in message news:3cf20663-960d-4ab1-9210-08042ca6af43@googlegroups.com... > On Tuesday, February 25, 2014 7:29:45 PM UTC-8, Anh Vo wrote: >> GNAT did not raise Assertion_Error where I thought it should for the >> following codes. Either I misunderstood the LRM or it is a compiler bug. > > It looks to me like this should work, according to 7.3.2(19). I don't > know what GNAT's > default Assertion_Policy for Type_Invariant'Class is, however. 7.3.2(19/3) is a mess, however. AI12-0042-1 changed it a lot, but that change isn't right either, so it's rather in limbo at the moment. (See the working RM for the current state of things.) Note that a literal implementation of 7.3.2(19/3) would cause every invariant check to go infinitely recursive, since there is supposed to be an invariant check on the parameter of Check_In, which is called from the invariant check - repeat forever. GNAT doesn't implement that for obvious reasons, so it can't exactly implement the rule as written, and once you have to go off the grid, all bets are off. Some parts will be in every rule (checking of in out and out parameters, for instance), so you probably can assume those are checked. But that's about it. Probably it would be better to not depend too much on Type_Invariants until we figure out what rules actually make sense (and we find a set that isn't insane for one reason or another). Randy.