Re: GNAT bug with assertions

[Anh Vo <anhvofrcaus@gmail.com>]

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