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: 
 Xl.tags.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 04 Mar 2015 16:42:26 -0600
Newsgroups: comp.lang.ada
Date: Wed, 4 Mar 2015 17:42:24 -0500
From: Peter Chapin <PChapin@vtc.vsc.edu>
X-X-Sender: pcc09070@WIL414CHAPIN.vtc.vsc.edu
Subject: Re: SPARK internal error?
In-Reply-To: <851b7d3c-4ac3-4fba-852d-c2975050da74@googlegroups.com>
Message-ID: <alpine.CYG.2.11.1503041735140.1588@WIL414CHAPIN.vtc.vsc.edu>
References: <851b7d3c-4ac3-4fba-852d-c2975050da74@googlegroups.com>
User-Agent: Alpine 2.11 (CYG 23 2013-08-11)
Organization: Vermont Technical College
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-WMdGD2qXyROXhuNxtno5+4xLb/mlJ8Onagk/7J/gJ4sHf9nMLaKAgw9uptBKd0Va/IGz5yIze/Dln6x!0Zq9/7PzxBWH4qXcGNpJ7rtJtv3lOguOKKb6vnaW+2P68iaHWz/PXviiwCCbVV33aWeMItilwJ+3!LUH/3njBZcvDuwoZdA==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2418
Xref: number.nntp.giganews.com comp.lang.ada:192418
Date: 2015-03-04T17:42:24-05:00
List-Id: <comp.lang.ada>

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