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
Path: 
 g2news1.google.com!postnews.google.com!e5g2000yqn.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Question about SPARK flow error.
Date: Sun, 20 Jun 2010 01:42:28 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <4ba6c1f7-8471-46b9-b6ae-22489b34066e@e5g2000yqn.googlegroups.com>
References: <4c1cf6a3$0$30803$4d3efbfe@news.sover.net>
 <78a3a0d8-9216-4c55-a586-162995f41046@q12g2000yqj.googlegroups.com>
	<4c1d627f$0$3623$4d3efbfe@news.sover.net>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1277023348 3973 127.0.0.1 (20 Jun 2010 08:42:28
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Sun, 20 Jun 2010 08:42:28 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: e5g2000yqn.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: g2news1.google.com comp.lang.ada:11832
Date: 2010-06-20T01:42:28-07:00
List-Id: <comp.lang.ada>

On 20 June, 01:37, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
> 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 proced=
ure
> off with
>
> =A0 =A0 =A0 =A0 Index :=3D 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.

That sounds like a reasonable solution in this case.

> 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 prob=
lem.
> However, at least I can initialize Index to a semantically meaningful val=
ue.

I think that there is sometimes a tendency to expect more of the
Examiner than it can deliver - eliminating flow errors does not
guarantee correctness of the code, it just reduces the opportunities
for errors.

There may be some mileage in using check annotations to justify the
use of accept annotations for data flow errors - I'm going to think
about that one a little more.

Cheers,

Phil