From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=0.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,bc2c82b1e5c6fe83,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.218.166 with SMTP id ph6mr2999416pbc.5.1330183151534;
        Sat, 25 Feb 2012 07:19:11 -0800 (PST)
Path: 
 h9ni7944pbe.0!nntp.google.com!news2.google.com!Xl.tags.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Sat, 25 Feb 2012 09:19:09 -0600
Date: Sat, 25 Feb 2012 10:19:02 -0500
From: "Peter C. Chapin" <PChapin@vtc.vsc.edu>
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64;
 rv:10.0.2) Gecko/20120216 Thunderbird/10.0.2
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Question about out parameters of unconstrained array type.
Message-ID: <I8qdndMrnK9zZtXS4p2dnAA@giganews.com>
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-RXluP+c7Ajwrz8lPfwuEOsq2e3RGdSy2sAhmdIfQmL0NLIkWD/RbDWBRUpGvUGBSQhQwtsxNdrtny0+!8X+qZYbSS2IfMldY8mSPrMBWgo1h3L8hLINsO0mYDgT3bolXlXDnnbevZM6hLCM=
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2139
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Date: 2012-02-25T10:19:02-05:00
List-Id: <comp.lang.ada>

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