--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on July 2010 ---
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 |