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

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

On 28 May, 10:00, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> [...] So I removed the L <= Length and left L >= 1  
> only, which was shown to be enough.
>
> Without you, I would not have been able to guess the trouble was there, as  
> to me, it was obvious L >= 1, as the type of L, which is really  
> Length_Type, has Length_Type'First = 1.
>
> This is still strange in some way, as if I do L >= Length_Type'First, it  
> works.
>
> So the Assert clause even drops implicit hypotheses about numeric type  
> bounds ? I was thinking this ones were preserved even after an Assert  
> clause.
>
> I was pretty sure Assert was still preserving somethings, as I feel I  
> remember I have read something suggesting that in one of the Praxis's  
> documentation and in yours as well (do not remember which PDF file, and  
> there many to check).

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).

So the fact that adding L >= Length_Type'First allows the Simplifier
to prove the check suggests that you are not getting these hypotheses
- possibly for one of the above reasons.

If you should be getting these hypotheses then post (or email) the
complete SPARKable code.

Cheers,

Phil