From: Simon Wright <simon@pushface.org>
Subject: Re: GNAT bug with assertions
Date: Fri, 10 Aug 2018 17:16:13 +0100
Date: 2018-08-10T17:16:13+01:00 [thread overview]
Message-ID: <lyd0uqyz76.fsf@pushface.org> (raw)
In-Reply-To: 87y3dejlq9.fsf@adaheads.home
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).
next prev parent reply other threads:[~2018-08-10 16:16 UTC|newest]
Thread overview: 12+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-08-10 10:29 GNAT bug with assertions AdaMagica
2018-08-10 14:23 ` Anh Vo
2018-08-10 15:16 ` Jacob Sparre Andersen
2018-08-10 16:16 ` Simon Wright [this message]
2018-08-10 20:42 ` Randy Brukardt
2018-08-12 18:35 ` AdaMagica
2018-08-12 18:51 ` Simon Wright
2018-08-13 9:03 ` AdaMagica
2018-08-13 9:07 ` Simon Wright
2018-08-13 15:54 ` Simon Wright
2018-08-13 16:55 ` Simon Wright
2018-08-14 2:37 ` AdaMagica
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox