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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Received: by 2002:a6b:d54b:: with SMTP id
 x11-v6mr2741245ioc.32.1533911015117;
        Fri, 10 Aug 2018 07:23:35 -0700 (PDT)
X-Received: by 2002:aca:4787:: with SMTP id
 u129-v6mr224704oia.4.1533911014980;
 Fri, 10 Aug 2018 07:23:34 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.uzoreto.com!newsreader4.netcologne.de!news.netcologne.de!peer03.ams1!peer.ams1.xlned.com!news.xlned.com!peer03.am4!peer.am4.highwinds-media.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!g13-v6no685204itf.0!news-out.google.com!g5-v6ni532iti.0!nntp.google.com!g13-v6no685197itf.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Fri, 10 Aug 2018 07:23:34 -0700 (PDT)
In-Reply-To: <a9ceb787-b964-4c53-91de-02bee039f6e5@googlegroups.com>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=24.6.20.197;
 posting-account=Qh2kiQoAAADpCLlhT_KTYoGO8dU3n4I6
NNTP-Posting-Host: 24.6.20.197
References: <a9ceb787-b964-4c53-91de-02bee039f6e5@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <fab0d2a8-098f-46bc-9728-841627ce3177@googlegroups.com>
Subject: Re: GNAT bug with assertions
From: Anh Vo <anhvofrcaus@gmail.com>
Injection-Date: Fri, 10 Aug 2018 14:23:35 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 2818
X-Received-Body-CRC: 461098579
Xref: reader02.eternal-september.org comp.lang.ada:54125
Date: 2018-08-10T07:23:34-07:00
List-Id: <comp.lang.ada>

On Friday, August 10, 2018 at 3:29:34 AM UTC-7, AdaMagica wrote:
> I would have expected that predicates are also checked on return values as they are checked on parameters.
> In the following test, no exception is raised on call of funcction Wrong although it returns a value not fulfilling the predicate.
> 
> Is this a GNAT bug or my wrong expectation?
> 
> package Pack is
> 
>   type Priv is private;
>   C: constant Priv;
> 
>   function Test (X: Priv) return Boolean;
>   subtype Subt is Priv with Dynamic_Predicate => (Test (Subt));
> 
>   function Wrong return Subt;
>   function Good (X: Subt) return Boolean;
> 
> private
> 
>   type Priv is new Integer;
>   C: constant Priv := -1;
> 
>   function Test (X: Priv) return Boolean is (X > 0);
> 
>   function Wrong return Subt is (-1);
>   function Good (X: Subt) return Boolean is (True);
> 
> end Pack; 
> 
> with Ada.Assertions, Ada.Text_IO;
> use  Ada.Assertions, Ada.Text_IO;
> 
> with Pack;
> use  Pack;
> 
> procedure Test_Pack is
> begin
> 
>   begin
>     Put_Line (Good (C)'Image);
>   exception
>     when Assertion_Error =>
>       Put_Line ("Good (C) raises Assertion_Error => OK");
>   end;
> 
>   declare
>     X: Priv;
>   begin
>     X := Wrong;
>     Put_Line ("Assertion_Error expected by calling Wrong => KO");
>   exception
>     when Assertion_Error =>
>       Put_Line ("Wrong raises Assertion_Error => OK");
>   end;
> 
> end Test_Pack;

I assume you used -gnata switch for your GNAT compilation. Otherwise, you will not see the effect.

Anh Vo