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] Assigns clause

  • Subject: [Frama-c-discuss] Assigns clause
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Wed, 25 Sep 2013 08:56:25 +0200
  • In-reply-to: <CAEtoXR1s3CaUoBjWjQkxjcz8PT4kLO7MOpKFpUEsf=13Zchh2g@mail.gmail.com>
  • References: <CAEtoXR1s3CaUoBjWjQkxjcz8PT4kLO7MOpKFpUEsf=13Zchh2g@mail.gmail.com>
Hello,

2013/9/24 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>:
> However, we would like to write a more precise assigns clause for the Interp
> array that has two or three elements according to Itab value.
>
> In the requires and ensures clauses the Itab value was considered, for
> example:
> requires Itab != 1 ==> \valid_range (Interp,0,2);
>
> requires Itab == 1 ==> \valid_range (Interp,0,1);
>
> How to write the assigns clause for the Interp array taking in account the
> Itab value?
>
The easiest way is to provide behaviors. Note in addition that
\valid_range has been deprecated. You should use
\valid instead:

/*@
    requires Itab == 0 || Itab == 1;
    behavior Itab_is_one:
    assumes Itab == 1;
    requires \valid(Interp + (0..1));
    assigns Interp[0..1];
    ...
    behavior Itab_is_zero:
    assumes Itab==0;
   requires \valid(Interp+(0..2));
   assigns Interp[0..2];
   ...
*/

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile