Re: SPARK internal error?

[joakim.strandberg@cxense.com]

On Tuesday, March 3, 2015 at 10:54:08 AM UTC+1, 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:
> 
> 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/

Dear Maciej,

Your probably already know this but I have found that the SPARK mailing list is a great place to ask SPARK questions:

http://lists.forge.open-do.org/pipermail/spark2014-discuss/

It is moderated but all questions I've posted so far have been accepted and answered shockingly fast by Yannick Moy (although there are other active users there too).

Best regards,
Joakim Strandberg