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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,c3f4071dbfa958f
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news1.google.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nx02.iad01.newshosting.com!newshosting.com!198.186.194.249.MISMATCH!transit3.readnews.com!news-out.readnews.com!postnews3.readnews.com!not-for-mail
Message-Id: <4c1d627f$0$3623$4d3efbfe@news.sover.net>
From: "Peter C. Chapin" <pcc482719@gmail.com>
Subject: Re: Question about SPARK flow error.
Newsgroups: comp.lang.ada
Date: Sat, 19 Jun 2010 20:37:48 -0400
References: <4c1cf6a3$0$30803$4d3efbfe@news.sover.net>
 <78a3a0d8-9216-4c55-a586-162995f41046@q12g2000yqj.googlegroups.com>
User-Agent: KNode/0.10.9
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7Bit
Organization: SoVerNet (sover.net)
NNTP-Posting-Host: 3db85a97.news.sover.net
X-Trace: 
 DXC=N\B;BnbE=J9TkVe4FPDeU7K6_LM2JZB_391LgWiP^@F;:WUUlR<856?[cOh[=T2T8;CAGNMH[X?22
X-Complaints-To: abuse@sover.net
Xref: g2news1.google.com comp.lang.ada:11827
Date: 2010-06-19T20:37:48-04:00
List-Id: <comp.lang.ada>

Phil Thornley wrote:

> The best way to deal with the error is an accept annotation.
> Such an annotation is a potential risk as it may hide a genuine data
> flow error (if not now then maybe when the code is changed at some
> point in the future).

Thanks for the suggestion. It sounds reasonable. What I did (at least for now)
is more like a "junk initialization" although perhaps not complete junk. If
the item is not found then Index gets Next_Index. So I started the procedure
off with

        Index := Next_Index;

and removed that assignment from the condition when the item is not found. If
the item is found inside the loop, Index gets overridden by a different
value. Note that Next_Index is definitely initialized properly; my
annotations declare it as a global in out variable and I have an
initialization procedure (elsewhere) that sets it up.

I can see the danger to this... if I forgot to set Index inside the loop (or
if that assignment gets removed later) the Examiner won't notice the problem.
However, at least I can initialize Index to a semantically meaningful value.

Peter