Re: SPARK internal error?

[Maciej Sobczak <see.my.homepage@gmail.com>]

> The following passes and makes gnatprove produce
> warning addressing range/pre/post/loop_invariant:
> 
>      procedure Sort (A : in out My_Array) is
>      begin
>          for I in A'Range loop
>              declare
>                  X : My_Array (I .. A'Last) := (others => 0);

Yes, in the line above. But why? We have a precondition that guarantees there are no empty slices here - and even without it, the fact that we are within the for loop over A'Range should already guarantee that both I and A'Last have safe values. Something is wrong here.

And of course, partially sorting a temporary array does not help in the proof that the main array becomes sorted as well...

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