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=-0.4 required=5.0 tests=AC_FROM_MANY_DOTS,BAYES_00,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Received: by 10.52.246.135 with SMTP id xw7mr30652496vdc.8.1425376447179;
        Tue, 03 Mar 2015 01:54:07 -0800 (PST)
X-Received: by 10.140.41.104 with SMTP id y95mr399632qgy.7.1425376447120; Tue,
 03 Mar 2015 01:54:07 -0800 (PST)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!peer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!w8no63514qac.0!news-out.google.com!n6ni191qar.0!nntp.google.com!w8no63510qac.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Tue, 3 Mar 2015 01:54:06 -0800 (PST)
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=31.186.238.53;
 posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S
NNTP-Posting-Host: 31.186.238.53
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <851b7d3c-4ac3-4fba-852d-c2975050da74@googlegroups.com>
Subject: SPARK internal error?
From: Maciej Sobczak <see.my.homepage@gmail.com>
Injection-Date: Tue, 03 Mar 2015 09:54:07 +0000
Content-Type: text/plain; charset=ISO-8859-1
X-Received-Bytes: 3697
X-Received-Body-CRC: 2813085160
Xref: news.eternal-september.org comp.lang.ada:25084
Date: 2015-03-03T01:54:06-08:00
List-Id: <comp.lang.ada>

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:

pragma SPARK_Mode;

package My_Package is

    type Index is range 1 .. 10;
    type My_Array is array (Index range <>) of Integer;
    
    procedure Find_Min (A : in My_Array; I : out Index)
        with Pre => A'First <= A'Last,
             Post =>
             (I in A'Range and
                (for all J in A'Range =>
                    A (I) <= A (J)));

    procedure Min_To_Left (A : in out My_Array)
        with Pre => A'First <= A'Last,
             Post =>
             (for all I in A'Range => A (A'First) <= A (I));
        
    procedure Sort (A : in out My_Array)
        with Pre => A'First <= A'Last,
             Post =>
             (for all I in A'Range =>
                (for all J in I .. A'Last =>
                   A (I) <= A (J)));

end My_Package;


Package body:

pragma SPARK_Mode;

package body My_Package is

    procedure Find_Min (A : in My_Array; I : out Index) is
        Last_Min : Integer;
    begin
        I := A'First;
        Last_Min := A (A'First);
        
        for J in A'First + 1 .. A'Last loop

            if A (J) < Last_Min then
                I := J;
                Last_Min := A (J);
            end if;

            pragma Loop_Invariant
                (for all K in A'First .. J =>
                    I in A'First .. J and Last_Min = A (I) and Last_Min <= A (K));
        end loop;
    end Find_Min;
    
    procedure Min_To_Left (A : in out My_Array) is
        I : Index;
        Tmp : Integer;
    begin
        Find_Min (A, I);
        
        Tmp := A (A'First);
        A (A'First) := A (I);
        A (I) := Tmp;
    end Min_To_Left;
    
    procedure Sort (A : in out My_Array) is
    begin
        for I in A'Range loop
            Min_To_Left (A (I .. A'Last));
            
            pragma Loop_Invariant
                (for all J in I .. A'Last =>
                        A (I) <= A (J));
        end loop;
    end Sort;

end My_Package;

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.


The my_package.mlw file has explicit content and is unappropriate for Usenet publication. ;-)

Can you reproduce it? Is it a bug in the toolset?
How can I work around it?

-- 
Maciej Sobczak * http://www.inspirel.com/