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 Newsgroups: comp.lang.ada Subject: Re: New to Spark, working an example Date: Sun, 16 Dec 2018 09:48:17 +0000 Organization: A noiseless patient Spider Message-ID: References: <6f00bf64-d501-487c-b3cb-17e97346e801@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: reader01.eternal-september.org; posting-host="a0f627ec4435de4aa3d98af4daa3e02e"; logging-data="16586"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18bWrVqcXFbteA9oJZW4OseeH8rHd5zrGQ=" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (darwin) Cancel-Lock: sha1:/bQ7V5LBuae0Iw7OQWk3DNgXjcg= sha1:kTy2AAHbGwafxMg7dMHH/JrYzHM= Xref: reader01.eternal-september.org comp.lang.ada:55050 Date: 2018-12-16T09:48:17+00:00 List-Id: I don't think there's anything wrong with trying to attract attention (what gets my goat a bit is people posting the same question in both places at the same time). I have to confess that I hadn't set up my SO account to watch the tags [spark-2014] or [spark-ada] (why both?), or even [gnat] or [ada2012] - rectified. You would have got more views if you'd included [ada] (but not necessarily any (more) answers :) Your problems are an indication of why I, as a person who has no access to professional SPARK support, haven't invested any effort to speak of in SPARK (my difficulties were with tasking/time rather than mathematical loops, which tend to be rare in control systems). That said, it looks to me as though the version of gnatprove in GNAT CE 2018 may not fully understand exponentiation: util.ads:3:14: medium: postcondition might fail, cannot prove 2 ** Floor_Log2'Result <= X util.ads:3:16: medium: overflow check might fail (e.g. when Floor_Log2'Result = 0)