Question about out parameters of unconstrained array type.

["Peter C. Chapin" <PChapin@vtc.vsc.edu>]

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 either have to 1) give the parameter 
mode in out or 2) initialize S inside the procedure before doing 
anything with it (for example with an aggregate). SPARK appears to 
behave as if the entire string is uninitialized upon entry into the 
procedure... even the attributes. I'm having trouble finding information 
about this in my SPARK references also.

Peter