[Spark2014-discuss] Foo'Result'First strange behavior

Yannick Moy moy at adacore.com
Tue Jul 22 14:19:55 CEST 2014

-- Hugues Jérôme (2014-07-22)
> The “strange” behavior I see is the following:
> - the two assertions are proved
> chap6.adb:61:7: info: assertion proved()
> chap6.adb:62:7: info: assertion proved()
> - but not the postcondition
> chap6.ads:61:18: warning: postcondition might fail, requires Reverse_Copy'Result'Last = X'last()
> AFAICT, the postcondition and the assertion refers to the same entity. Is it a known limitation in the toolset?

Yes, there are limitations in the GPL 2014 version wrt proof of unconstrained arrays. This has been much improved in the current development version, and I can now prove your code completely. 
Yannick Moy, Senior Software Engineer, AdaCore

More information about the Spark2014-discuss mailing list