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=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,b49755ab898bcffd
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!v18g2000vbc.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK again : for-loop vs single loop - a strange case
Date: Fri, 28 May 2010 08:13:57 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <22bd64db-4c71-4856-a60f-f9b2411ab23b@v18g2000vbc.googlegroups.com>
References: <op.vddp3fvvxmjfy8@garhos>
 <2b6ae662-77e2-4d1a-a2b2-3df54f8ab98e@v37g2000vbv.googlegroups.com>
	<op.vderaoe5ule2fv@garhos>
 <eb1871bc-62d0-411c-b96e-97f8c8e148f6@f14g2000vbn.googlegroups.com>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
X-Trace: posting.google.com 1275059637 8553 127.0.0.1 (28 May 2010 15:13:57
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 28 May 2010 15:13:57 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: v18g2000vbc.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
	Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
	3.0.30729; Media Center PC 6.0),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:12128
Date: 2010-05-28T08:13:57-07:00
List-Id: <comp.lang.ada>

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