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