Prev: What Ada can do for Cryptography.
Next: Advice on selling Ada to a C shop
From: Peter C. Chapin on 19 Jun 2010 12:58
My example isn't complete enough to compile, but I could work up a complete
example if necessary. Hopefully this will be accurate and complete enough...

Consider the following procedure:

procedure Add_Item
(Item : in Some_Type; Index : out Index_Type) is

Found : Boolean;
begin
Found := False;

-- Let's see if the Item already exists in the storage.
for I in Index_Type range Index_Type'First .. Size loop
if Storage(I) = Item then
Index := I; -- It does. Return the current position.
Found := True;
exit;
end if;
end loop;

if not Found then
-- The Item does not already exist. Install it in the next slot.
Storage(Next_Index) := Item;
Index := Next_Index; -- Return where we installed it.

-- Play around with Size and Next_Index to set them up for next time
-- (not shown).
end if;
end Add_Item;

SPARK gives me an error, "Flow Error 602 - The undefined initial value of
Index may be used in the derivation of Index." I understand this to mean that
there is a path through the procedure where Index (being an out parameter) is
never given a value. So SPARK might be thinking, "Okay... the loop might run
to completion without ever setting Index inside the inner conditional
statement. Then it might skip over the next conditional statement and thus
never set Index at all."

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?

Thanks

Peter

From: Phil Thornley on 19 Jun 2010 14:03
On 19 June, 17:58, "Peter C. Chapin" <pcc482...(a)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
From: Gavino on 19 Jun 2010 14:14
"Peter C. Chapin" <pcc482719(a)gmail.com> wrote in message
news:4c1cf6a3$0$30803$4d3efbfe(a)news.sover.net...
> 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?
Flow analysis is only concerned with syntactically possible paths through
the code and does not consider semantic aspects such as this.
For that level of analysis, you need to use the SPARK proof tools.

You could shut the Examiner up by initialising Index (eg to
Index_type'First), but it doesn't seem a satisfactory solution.


From: Gavino on 19 Jun 2010 14:23
"Phil Thornley" <phil.jpthornley(a)gmail.com> wrote in message
news:fd3e54b4-bff0-470a-8409-f48c3289a2f3(a)x27g2000yqb.googlegroups.com...
> 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).

Doesn't that just push the flow error onto Local_Index?
After all, the loop body itself may (in principle) never be executed.


From: Phil Thornley on 19 Jun 2010 15:24
On 19 June, 19:23, "Gavino" <inva...(a)invalid.invalid> wrote:
> "Phil Thornley" <phil.jpthorn...(a)gmail.com> wrote in message
>
> news:fd3e54b4-bff0-470a-8409-f48c3289a2f3(a)x27g2000yqb.googlegroups.com...
>
> > 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).
>
> Doesn't that just push the flow error onto Local_Index?
> After all, the loop body itself may (in principle) never be executed.

Ummm, yes, you're probably right :-(

(Just shows that I should have stuck to my normal policy of not
pronouncing on what the Examiner will do without checking it first on
real code).

Cheers,

Phil
 |  Next  |  Last
Pages: 1 2
Prev: What Ada can do for Cryptography.
Next: Advice on selling Ada to a C shop