--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on July 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with loop invariant



Boris Hollas wrote:
> On Mon, 2010-06-28 at 14:04 +0200, n.rousset at laposte.net wrote:
>   
>> The loop invariant after the loop body is indeed equivalent to the
>> assertion,
>> but the invariant is checked AFTER the assertion...
>>     
>
> what does this explain?
>
>   
The verification conditions are generated following this shape :

//@ assume <the loop invariant>

sreadi(msg_send,tosend,internal.msgnum);
abpRound(msg_send,msg_receive,&channel,&internal);
swritei(received,msg_receive,internal.msgnum);

//@ assert \forall integer x; 0 <= x < (internal.msgnum+1) * BUFFSIZE
==> tosend->data[x] == received->data[x];

internal.msgnum++

//@ assert <the loop invariant>

So as said Nicolas, proving the loop invariant preservation is straghtforward since the assertion is assumed
to be checked before.





>> To find out why the assertion is not proved,
>> we need to see the postconditions of sreadi(), abpRound(), and
>> swritei().
>>     
Please check that the given post-conditions are enough to prove

tosend->data[x] == received->data[x];

when internal.msgnum * BUFFSIZE <= x < (internal.msgnum+1) * BUFFSIZE

because it is just this part of x interval that might causes problems.

- Claude

-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |