--- layout: fc_discuss_archives title: Message 129 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Assigns clause



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