Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with loop invariant

  • Subject: [Frama-c-discuss] Problem with loop invariant
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Fri, 09 Jul 2010 10:58:32 +0200
  • In-reply-to: <1277728372.1482.21.camel@iti27>
  • References: <1276795121.1681.16.camel@iti27> <4C1F2AF5.3000604@inria.fr> <1277298042.2073.36.camel@iti27> <14634911.194632.1277726661282.JavaMail.www@wwinf8302> <1277728372.1482.21.camel@iti27>
Boris Hollas wrote:
> 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?
>
>   
The verification conditions are generated following this shape :

//@ assume <the loop invariant>

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];

internal.msgnum++

//@ assert <the loop invariant>

So as said Nicolas, proving the loop invariant preservation is straghtforward since the assertion is assumed
to be checked before.





>> To find out why the assertion is not proved,
>> we need to see the postconditions of sreadi(), abpRound(), and
>> swritei().
>>     
Please check that the given post-conditions are enough to prove

tosend->data[x] == received->data[x];

when internal.msgnum * BUFFSIZE <= x < (internal.msgnum+1) * BUFFSIZE

because it is just this part of x interval that might causes problems.

- Claude

-- 
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                    |