--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on June 2010 ---
Now, the code verifies. However, there are two points that I can't explain: - The loop invariant can be proved, but not the assertion at the end of the loop body. But the latter should follow from the loop invariant because wp(internal.msgnum++, \forall integer x; 0 <= x < internal.msgnum * BUFFSIZE ==> tosend->data[x] == received->data[x];) = \forall integer x; 0 <= x < (internal.msgnum+1) * BUFFSIZE ==> tosend->data[x] == received->data[x]; where wp(S,P) is the weakest precondition of S wrt P. - If the assertion is omitted, the loop invariant can't be proved. Does it nonetheless cause the prover to find the right goals? /*@ 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]; } -- Regards, Boris