Re: Question about SPARK flow error.

["Peter C. Chapin" <pcc482719@gmail.com>]

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