GNAT bug with assertions

GNAT bug with assertions

[AdaMagica]

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;

Re: GNAT bug with assertions

[Anh Vo]

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

Re: GNAT bug with assertions

[Jacob Sparre Andersen]

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?

It seems that your expectations are slightly off.

Contracts are only checked if the assertion policy is set to "Check".
You can do that, either by configuring your compiler to have the
assertion policy set to "Check", or by explicitly inserting:

   pragma Assertion_Policy (Check);

at the beginning of the units, which should have this assertion policy.

If I remember correctly, setting the assertion policy of a package
specification to "Check" means that the contracts of the subprograms
specified in the package are checked, even if they are called from a
unit with assertion policy "Ignore".

Greetings,

Jacob
-- 
Computers are not intelligent.  They only think they are.

Re: GNAT bug with assertions

[Simon Wright]

Jacob Sparre Andersen <jacob@jacob-sparre.dk> writes:

> 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?
>
> It seems that your expectations are slightly off.

Or perhaps you, Jacob, have a later release of the compiler which has
this bug fixed?

> Contracts are only checked if the assertion policy is set to "Check".
> You can do that, either by configuring your compiler to have the
> assertion policy set to "Check", or by explicitly inserting:
>
>    pragma Assertion_Policy (Check);
>
> at the beginning of the units, which should have this assertion policy.

Or, in the case of GNAT, by giving -gnata: see
http://docs.adacore.com/gnat_ugn-docs/html/gnat_ugn/gnat_ugn/building_executable_programs_with_gnat.html#debugging-and-assertion-control

If Cristoph hadn't been using -gnata, the first check would have failed.

IMO this is a bug in GNAT, present in CE2018 and FSF GCC 8 (and maybe
earlier, didn't check).

Re: GNAT bug with assertions

[Randy Brukardt]

"Simon Wright" <simon@pushface.org> wrote in message 
news:lyd0uqyz76.fsf@pushface.org...
...
> IMO this is a bug in GNAT, present in CE2018 and FSF GCC 8 (and maybe
> earlier, didn't check).

Looks likely (I didn't check the wording to be certain). Predicate checks 
should occur any time there is a conversion of an entire object to the 
appropriate subtype, and that should happen in a return statement.

                                        Randy.

Re: GNAT bug with assertions

[AdaMagica]

Thank you all for your time to think about this.

I'll send it in to AdaCore. Hopefully it will be correted next year in the public version.

Re: GNAT bug with assertions

[Simon Wright]

AdaMagica <christ-usch.grein@t-online.de> writes:

> Thank you all for your time to think about this.
>
> I'll send it in to AdaCore. Hopefully it will be correted next year in
> the public version.

This is a somewhat artificial error, isn't it?

   function Maybe (X : Priv) return Subt;
   ...
   function Maybe (X : Priv) return Subt is (X);
   ...
   X := Maybe (C);   -- C is -1

works as we would have expected.

Re: GNAT bug with assertions

[AdaMagica]

Am Sonntag, 12. August 2018 20:51:51 UTC+2 schrieb Simon Wright:
> AdaMagica writes:
> 
> > Thank you all for your time to think about this.
> >
> > I'll send it in to AdaCore. Hopefully it will be correted next year in
> > the public version.
> 
> This is a somewhat artificial error, isn't it?
> 
>    function Maybe (X : Priv) return Subt;
>    ...
>    function Maybe (X : Priv) return Subt is (X);
>    ...
>    X := Maybe (C);   -- C is -1
> 
> works as we would have expected.

What is it that you expect here? What type is X? I didn't try with GNAT, but I would expect Maybe (C) to raise Assertion_Error independently of X.

Re: GNAT bug with assertions

[Simon Wright]

AdaMagica <christ-usch.grein@t-online.de> writes:

> Am Sonntag, 12. August 2018 20:51:51 UTC+2 schrieb Simon Wright:
>> AdaMagica writes:
>> 
>> > Thank you all for your time to think about this.
>> >
>> > I'll send it in to AdaCore. Hopefully it will be correted next year
>> > in the public version.
>> 
>> This is a somewhat artificial error, isn't it?
>> 
>>    function Maybe (X : Priv) return Subt;
>>    ...
>>    function Maybe (X : Priv) return Subt is (X);
>>    ...
>>    X := Maybe (C);   -- C is -1
>> 
>> works as we would have expected.
>
> What is it that you expect here? What type is X? I didn't try with
> GNAT, but I would expect Maybe (C) to raise Assertion_Error
> independently of X.

Oh come on! these are additions to the example that *you* posted upthread.

Re: GNAT bug with assertions

[Simon Wright]

Simon Wright <simon@pushface.org> writes:

> AdaMagica <christ-usch.grein@t-online.de> writes:
>
>> Am Sonntag, 12. August 2018 20:51:51 UTC+2 schrieb Simon Wright:
>>> AdaMagica writes:
>>>
>>> > Thank you all for your time to think about this.
>>> >
>>> > I'll send it in to AdaCore. Hopefully it will be correted next year
>>> > in the public version.
>>>
>>> This is a somewhat artificial error, isn't it?
>>>
>>>    function Maybe (X : Priv) return Subt;
>>>    ...
>>>    function Maybe (X : Priv) return Subt is (X);
>>>    ...
>>>    X := Maybe (C);   -- C is -1
>>>
>>> works as we would have expected.
>>
>> What is it that you expect here? What type is X? I didn't try with
>> GNAT, but I would expect Maybe (C) to raise Assertion_Error
>> independently of X.
>
> Oh come on! these are additions to the example that *you* posted upthread.

Oops.

X is of type Subt.

It can get quite misleading to use expression functions when trying to
use the debugger to work out where an exception is raised.

Given

   function Maybe (X : Priv) return Subt is
   begin
      return X;
   end Maybe;

called as

   S : Subt := Maybe (-);
   
Maybe happily returns -1 and leaves it up to the assignment to raise the
necessary exception.

And if the assignment is

   P : Priv := Maybe (-1);

no exception is raised.

Re: GNAT bug with assertions

[Simon Wright]

Simon Wright <simon@pushface.org> writes:

>    S : Subt := Maybe (-);

   S : Subt := Maybe (-1);

Not doing well today.

Re: GNAT bug with assertions

[AdaMagica]

Am Montag, 13. August 2018 17:54:28 UTC+2 schrieb Simon Wright:
>    function Maybe (X : Priv) return Subt is
>    begin
>       return X;
>    end Maybe;
> 
> called as
> 
>    S : Subt := Maybe (-1);
>    
> Maybe happily returns -1 and leaves it up to the assignment to raise the
> necessary exception.
> 
> And if the assignment is
> 
>    P : Priv := Maybe (-1);
> 
> no exception is raised.

Yes, this is what currently happens. Assertion_Error should instead be raised in both cases by Maybe.