Re: Question about SPARK flow error.

[Phil Thornley <phil.jpthornley@gmail.com>]

On 19 June, 17:58, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
[...]
> However, if I'm not mistaken that can't actually happen. If the conditional
> statement inside the loop never runs, Found will still be False and the
> second conditional will definitely execute. Index will receive a value either
> inside the loop or later.
>
> Am I missing something or is this reasoning outside of the abilities of
> SPARK's flow analysis? Is there some other idiomatic way I should be handling
> this sort of situation?

This is, really, outside what the Examiner does in flow analysis - it
doesn't look at the executability of paths when reporting flow errors.
(That's why the error says "... may be used ...".)

So there is a path through the flow graph of the procedure, even
though it can never be executed in practice.

One way to get rid of the error is to introduce a 'Local_Index' that
is set in the loop; then set Index to that value after the loop if
Found is True (and your existing code if False).

Alternatively, you can add an accept annotation for the error.

There shouldn't be any risk of the accept annotation allowing an error
through as, if there is a 'real' path through the code that doesn't
set Index then there should be an unprovable VC generated by the exit
run-time check VC for that path.  So the non-existence of an
unprovable VC supports the accept annotation.
(However I want to try this on some real code before making a firm
statement, Ill try that sometime soon.)

Cheers,

Phil