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



Boris Hollas wrote:
> Hello,
>
> in the loop below, both assertion can be verified, but not the loop
> invariant. The assertions are the same as the 3rd loop invariant that
> can't be proved. Since the assertion holds (as proved by Jessie) both at
> the beginning and at the end of the loop body, I don't understand why
> the loop invariant can't be proved.
>   
I guess it is because

   internal.msgnum++

is executed between the second assert and the loop invariant 
preservation checking

- Claude
> I should have used integer instead of int in the specification, btw.
>
> /*@
> 	loop variant MSGCOUNT - internal.msgnum;
> 	loop invariant 0 <= internal.msgnum &&
> 		\forall int x; 0 <= x < internal.msgnum ==>
>                        tosend->data[x] == received->data[x];
> 	*/
> for (internal.msgnum = 0;internal.msgnum < MSGCOUNT; internal.msgnum++)
> {
> 	//@ assert \forall int x; 0 <= x < internal.msgnum ==>
>                          tosend->data[x] == received->data[x];
> 	sreadi(msg_send,tosend,internal.msgnum);
> 	abpRound(msg_send,msg_receive,&channel,&internal);
> 	swritei(received,msg_receive,internal.msgnum);
> 	//@ assert \forall int x; 0 <= x < internal.msgnum ==>
>                          tosend->data[x] == received->data[x];
> }
>
>
>   


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |