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] Validity of an array of struct

Hello,

2012/11/11 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>:
> I would like to insert a pre-condition (\valid) related with an array of
> structs:

You generally don't need that: by construction, an array has valid
locations (up to its declared length of course).

> I did some attempts but they didn't work:
>

It would be clearer if for each attempt you described _exactly_ what
you expected and what you got.

> /* @ requires \valid(G_E+(0..5-1).G_Tratado);
>  @ requires  \valid(G_E+(0..5-1).G_Ativo);
>  @ requires  \valid(G_E+(0..5-1).G_Inst_Ativ);
> */

This is ill-typed: G_E+(0..5) is a set of pointers to the struct, you
should use either G_E+(0..5)->G_Tratado or  G_E[0..5].G_Tratado. And
even in that case, I don't think it means what you think: you have in
addition to take the addresses of the field to denote that each of
them is valid \valid(&(G_E[0..5-1].G_Tratado)).

>
> or
>
> /*@ requires \valid_range(G_E,0,4);*/
>
> or
>
> /*@ requires \valid(G_E+(0..5-1));*/
>

Both annotations are equivalent except that \valid_range is
deprecated. That said, as mentioned above, since G_E is a global array
of length 5, they are trivially true.

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