--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on June 2010 ---
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? > To find out why the assertion is not proved, > we need to see the postconditions of sreadi(), abpRound(), and > swritei(). Here again is the loop together with the assertion that doesn't verify: /*@ loop variant MSGCOUNT - internal.msgnum; loop invariant 0 <= internal.msgnum && \forall integer x; 0 <= x < internal.msgnum * BUFFSIZE ==> tosend->data[x] == received->data[x]; */ for (internal.msgnum = 0;internal.msgnum < MSGCOUNT; internal.msgnum++) { 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]; } The contracts for sreadi, abpRound, swritei are below. We use a twodimensional array "data" because Frama-C can't handle multidimensional arrays yet. The contract for sreadi is: /*@ requires \valid(buf); requires \valid(buf->data+(0.. BUFFSIZE*MSGCOUNT)); requires \valid(target+(0.. BUFFSIZE)); requires 0 <= idx < MSGCOUNT; ensures \forall int x; 0 <= x < BUFFSIZE ==> target[x] == buf->data[idx*BUFFSIZE + x]; ensures \forall int x; 0 <= x < BUFFSIZE*MSGCOUNT ==> buf->data[x] == \old(buf->data[x]); ensures target[BUFFSIZE] == 0; */ void sreadi(char* target, DataBuffer* buf, int idx) The contract for abpRound is: /*@ requires \valid(msg_send+(0.. BUFFSIZE)); requires \valid(msg_receive+(0.. BUFFSIZE)); requires \valid(channel); requires \valid(channel->msgChannel+(0.. BUFFSIZE+1)); requires \valid(internal); ensures \forall int x; 0 <= x < BUFFSIZE ==> msg_receive[x] == msg_send[x]; */ void abpRound(char *msg_send, char *msg_receive, ChannelType *channel, InternalType *internal) The contract for swritei is: /*@ requires \valid(buf); requires \valid(buf->data+(0.. BUFFSIZE*MSGCOUNT)); requires \valid(source+(0.. BUFFSIZE)); requires 0 <= idx < MSGCOUNT; ensures \forall int x; 0 <= x < BUFFSIZE ==> buf->data[idx*BUFFSIZE + x] == source[x]; ensures \forall int x; 0 <= x < idx*BUFFSIZE ==> buf->data[x] == \old(buf->data[x]); ensures buf->data[BUFFSIZE*MSGCOUNT] == 0; */ void swritei(DataBuffer* buf, char* source, int idx) BTW, on another computer also using Boron, the loop invariant above didn't verify. -- Regards, Boris