Re: SPARK again : for-loop vs single loop - a strange case

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 28 May, 12:50, Phil Thornley <phil.jpthorn...@googlemail.com>
wrote:
> This thread persuaded me to finally check precisely what the Examiner
> generates for local variables (I have always just assumed that it
> doesn't do anything - looking back through the release notes, this
> changed in Release 7.2).
>
> The statement about this is in GenRTCs section 4.5.2.1; hypotheses are
> generated that local variables are in-type if various conditions are
> met that ensure that no out-of-type value can be assigned in the
> procedure (no 'significant' data flow errors, no read from external
> variables and no use of Unchecked_Conversion).

I seem to have reproduced the same problem as Yannick.

Here is the code:

   subtype Index is Integer range 1 .. 10;
   type Arr is array(Index) of Integer;

   procedure Zero_Part (A : in out Arr;
                        U : in     Index)
   --# derives A from *, U;
   is
      I : Index;
   begin
      I := 1;
      loop
         A(I) := 0;
         exit when I >= U;
         I := I + 1;
      end loop;
   end Zero_Part;

As I understand the documentation the default assertion should include
hypotheses that I is in-type, but when simplified there are two
conclusions left for the A(I) := 0; assignment:
C1:    i >= 1 .
C2:    i <= 10 .

If I add the assertion:
--# assert I in Index;
then these conclusions are proved by the Simplifier.

So either my understanding of how the Examiner generates hypotheses is
wrong or the Examiner is wrong.

Cheers,

Phil