--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on June 2010 ---
> > 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>