--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on November 2012 ---
[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