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] read from and write on the same array

  • Subject: [Frama-c-discuss] read from and write on the same array
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Mon, 16 Feb 2009 15:05:55 +0100
  • In-reply-to: <0DF661750C2F4CDA9F3D9AF9B4776DB3@AHARDPLACE>
  • References: <0DF661750C2F4CDA9F3D9AF9B4776DB3@AHARDPLACE>
Le lun 16 f?v 2009 10:38:28 CET,
"Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit :

> From what I understood of the recent mails, it is difficult to read and write on the same memory location and to prove something about it.
> (Please correct me if I am wrong)

This is not exactly true. the jessie plugin does not have any issue
proving something about a location which is both read and written, as
long as it knows precisely which locations are written and which aren't.
Trouble arises when it (or the underlying theorem provers) can't decide
if a given location has still its old value or has just been assigned a
new one, for instance when you write to t[i] and read from t[k] without
knowing whether i and k are equal or distinct.

>     /*@
>      loop invariant 0  <= i <= length;
> 
>      loop invariant \forall integer k;  0 <= k < i ==>
>        (\at(a[k],Pre) == old_value ==>
>        a[k] == new_value);   
>     */
>     for (; i != length; ++i)
>     {
>         if (a[i] == old_value)
>         {
>             a[i] = new_value;
>         }
>     }
> }

You don't specify enough the effect of a loop step: from your
invariant, we know what happens to the cell whose initial value is
old_value, but nothing more. We have to tell the jessie plugin that the
other cells are left untouched. There are two ways to do that
- the simplest one is unfortunately not supported by the plugin yet: 
loop assigns a[i]; indicates in ACSL that at each step, only a[i] might
be modified
- we must thus add an invariant saying that all the cells beyond i still
have their initial value:
loop invariant \forall integer k; i <= k < length ==>
  a[k] == (\at[k],Pre);

Best regards,

-- 
E tutto per oggi, a la prossima volta.
Virgile