From: Simon Wright <simon@pushface.org>
Subject: Re: New to Spark, working an example
Date: Wed, 19 Dec 2018 16:58:41 +0000
Date: 2018-12-19T16:58:41+00:00 [thread overview]
Message-ID: <lyimzpe9mm.fsf@pushface.org> (raw)
In-Reply-To: 8bd49bc7-ea3e-4e8c-9292-c37fd2e54e54@googlegroups.com
Brad Moore <bmoore.ada@gmail.com> writes:
> On Sunday, December 16, 2018 at 2:48:19 AM UTC-7, Simon Wright wrote:
>> util.ads:3:16: medium: overflow check might fail (e.g. when
>> Floor_Log2'Result = 0)
> As an aside, it appears the version of gnatprove in GNAT CE 2018 does
> have a pretty good understanding of exponentiation, given that I was
> able to get the following proven.
Apparently so. But the part of gnatprove that gives examples of when the
assertion might fail is quite misleading: for example,
util.ads:7:14: medium: postcondition might fail, cannot prove 2 **
Floor_Log2'Result <= X (e.g. when Floor_Log2'Result = 0 and X = 0)
*when X is Positive* !! and
util.adb:19:15: medium: overflow check might fail (e.g. when I = 0)
l.18 for I in 1 .. Log_Result'Last loop
l.19 if 2 ** I > X then
next prev parent reply other threads:[~2018-12-19 16:58 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-12-16 5:43 New to Spark, working an example addaon
2018-12-16 9:48 ` Simon Wright
2018-12-19 2:41 ` Brad Moore
2018-12-19 16:58 ` Simon Wright [this message]
2018-12-20 4:34 ` Brad Moore
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox