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

[Frama-c-discuss] Problem with loop invariant



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