--- layout: fc_discuss_archives title: Message 54 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



> > 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 loop invariant is proved because the assertion is used as hypothesis (I think you can check this in the gui).
The assertion remains to be proved...

> /*@
> 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)
>

OK,
the assertion tells that the loop body must verify forall A * B <= x <= (A + 1) * B, P(x)
and the postconditions tells that forall 0 <= y <= B, P(A * B + y)

I guess provers have trouble to see that the two formulas are equivalent.
First issue : the variable bounds
Second issue: distributivity rule

Try to harmonize the specifications and it should work.

- Nicolas

Une messagerie gratuite, garantie ? vie et des services en plus, ?a vous tente ?
Je cr?e ma bo?te mail www.laposte.net
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100628/768eed0d/attachment.htm>