Re: New to Spark, working an example

[Simon Wright <simon@pushface.org>]

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)