Re: SPARK internal error?

[Peter Chapin <PChapin@vtc.vsc.edu>]

On Tue, 3 Mar 2015, Maciej Sobczak wrote:

> As a continuation of my previous post, here is the complete package with 
> the array sorting exercise (not sure if it's correct):
>
> Package spec:
>
> [...]
>
> Package body:
>
> [...]
>
> GNATprove says:
>
> C:\maciej\temp\spark>gnatprove -Ptest -q
> Internal error:
> File "C:\maciej\temp\spark\gnatprove\my_package\..\my_package.mlw", line 2094, characters 208-235:
> This term has type tindexB, but is expected to have type int.
> Aborting.
> gprbuild: *** compilation phase failed
> gnatprove: error during generation and proof of VCs, aborting.
>
> Can you reproduce it? Is it a bug in the toolset?

Apparently. I executed gnatprove successfully on your sample code. I'm 
using version

     16.0.0w (20141212)

This is a wavefront version. As far as I know its capabilities should be 
available in SPARK GPL 2015 (I'm not an AdaCore employee so I don't know 
anything for sure about their release schedule).

BTW, I get the following message from gnatprove:

sandbox.ads:25:20: medium: postcondition might fail, requires A (I) <= A 
(J)

So it's having problems with the postcondition of Sort.

Peter