Re: Question about SPARK flow error.

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

On 19 June, 17:58, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
[...]
Well, I was also wrong about using the non-existence of an unprovable
VC as evidence to support an accept annotation!

Using your code, the Simplifier proves all the VCs - and it still does
even if I remove either of the assignments to Index (and so create a
genuine data flow error).

The 'exit' VCs for a procedure are "trivially true" unless there is a
post-condition.  All exported values are assumed to be valid at this
point because the RTC analysis ***assumes that there are no data-flow
errors*** - i.e.:
1. all exports must have been assigned a value (otherwise there will
be a data-flow error), and
2. all values assigned must be valid otherwise there will be an
unprovable VC.

So it seems to me that:
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).

Consequently it makes sense to force a check on the relevant value by
adding a check annotation.

So, how about adding the following at the end of your procedure:
   --# accept F, 602, Index, Index,
   --#        "The following check ensures that there is no actual
error.";
   --# check Index in Index_Type;
end Add_Item;

This eliminates the reported flow error, and creates an unprovable VC
if there is any genuine data flow error for Index.
(It also needs a assertion in the loop: --# assert not Found;)

HTH

Phil