Re: Question about out parameters of unconstrained array type.

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

In article <I8qdndMrnK9zZtXS4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu 
says...
> 
> Consider a simple procedure
> 
> procedure P(S : out String) is
> begin
>     ...
> end P;
> 
> Despite the fact that S behaves as if it is uninitialized my Ada 
> compiler (GNAT GPL 2011) allows me to read certain attributes. For 
> example if the body is
> 
>    for I in 1 .. S'Length loop ...
> 
> (never mind that I'm making a bad assumption about S'First being 1) I 
> don't see any warning about reading an uninitialized value when I do 
> S'Length. This is fine but I'm having trouble locating in the LRM where 
> this behavior is explicitly said to be well defined. Is it well defined? 
> Where does it say so?
> 
> The reason I'm asking is because SPARK does *not* like the usage of 
> S'Length in my example above.

I think that you may be misinterpreting the SPARK error message:

  15        for I in 1 .. S'Length loop
                     ^
***        Syntax Error      : reserved word "IN" cannot be followed by
           INTEGER_NUMBER here.

The error here is that the loop index has an anonymous subtype.

If you change this to:

   for I in Integer range 1 .. S'Length loop

there is no syntax or semantic error reported. (You will get the usual 
flow error if you assign individual values of the string in the loop, 
but that's another problem all together.)

In fact the LRM states that this usage is permitted. See Section 4.1:
"... the name of an unconstrained array object (formal parameter) shall 
only appear in the following contexts:
   1  as the prefix of an attribute reference;
   2  ..."

Cheers,

Phil