--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on June 2010 ---
Boris Hollas wrote: > Hello, > > in the loop below, both assertion can be verified, but not the loop > invariant. The assertions are the same as the 3rd loop invariant that > can't be proved. Since the assertion holds (as proved by Jessie) both at > the beginning and at the end of the loop body, I don't understand why > the loop invariant can't be proved. > I guess it is because internal.msgnum++ is executed between the second assert and the loop invariant preservation checking - Claude > I should have used integer instead of int in the specification, btw. > > /*@ > loop variant MSGCOUNT - internal.msgnum; > loop invariant 0 <= internal.msgnum && > \forall int x; 0 <= x < internal.msgnum ==> > tosend->data[x] == received->data[x]; > */ > for (internal.msgnum = 0;internal.msgnum < MSGCOUNT; internal.msgnum++) > { > //@ assert \forall int x; 0 <= x < internal.msgnum ==> > tosend->data[x] == received->data[x]; > sreadi(msg_send,tosend,internal.msgnum); > abpRound(msg_send,msg_receive,&channel,&internal); > swritei(received,msg_receive,internal.msgnum); > //@ assert \forall int x; 0 <= x < internal.msgnum ==> > tosend->data[x] == received->data[x]; > } > > > -- 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 |