Prev: What Ada can do for Cryptography.
Next: Advice on selling Ada to a C shop
From: Phil Thornley on 19 Jun 2010 15:29
On 19 June, 19:14, "Gavino" <inva...(a)invalid.invalid> wrote:
[...]
> You could shut the Examiner up by initialising Index (eg to
> Index_type'First), but it doesn't seem a satisfactory solution.

The problem with this solution (which Peter Amey always referred to as
a 'junk initialisation' - an excellent name) is that it can hide a
genuine data flow error if there really is a path that does not give
Index a value.

Cheers,

Phil
From: Phil Thornley on 19 Jun 2010 19:28
On 19 June, 17:58, "Peter C. Chapin" <pcc482...(a)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
From: Peter C. Chapin on 19 Jun 2010 20:37
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

From: Phil Thornley on 20 Jun 2010 04:42
On 20 June, 01:37, "Peter C. Chapin" <pcc482...(a)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 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.

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 problem.
> However, at least I can initialize Index to a semantically meaningful value.

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
First  |  Prev  | 
Pages: 1 2
Prev: What Ada can do for Cryptography.
Next: Advice on selling Ada to a C shop