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=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: New to Spark, working an example
Date: Wed, 19 Dec 2018 16:58:41 +0000
Organization: A noiseless patient Spider
Message-ID: <lyimzpe9mm.fsf@pushface.org>
References: <6f00bf64-d501-487c-b3cb-17e97346e801@googlegroups.com>
	<lyh8fdby5a.fsf@pushface.org>
	<8bd49bc7-ea3e-4e8c-9292-c37fd2e54e54@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader01.eternal-september.org;
 posting-host="39291fe19961cb1c0e57f1c21605923e";
	logging-data="13466"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX183eFLzzm5V4o1PfGUAiQFdqQtCi5yDs+M="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (darwin)
Cancel-Lock: sha1:BWSFBMFSD4eU4phlm0U7bKQ0K5k=
	sha1:v21QRgQ2EYtlf2NyhVa73cg0rkA=
Xref: reader01.eternal-september.org comp.lang.ada:55080
Date: 2018-12-19T16:58:41+00:00
List-Id: <comp.lang.ada>

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