--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on November 2012 ---
Thank you, but I am confusing yet. I understood your comment : " You generally don't need that: by construction, an array has valid locations (up to its declared length of course). " But Jessie produces 2 VCs related to pointer dereferencing. I think that it is necessary to write annotations to prove them, isn't? What is wrong my rationale? If I run the Jessie without annotation I have 2 VCs and the follow VC is not proved: pointer dereferencing offset_min(__anonstruct_G_E_l_G_E_l_alloc_table,G_E) <=il Wtih the follow annotation, I didn't get to run. I am using the Carbon version. The follow message is showed: " File "ro.jc", line 48, characters 48-61: typing error: unbound term identifier __framac_tmp1 " I attached the source code. What is the solution for my verification? Thanks a lot, Rovedy //-------------------------------------------------------------------- float Tempo; #define FALSE 0 #define TRUE 1 #pragma JessieIntegerModel(math) #pragma JessieTerminationPolicy(user) #pragma JessieFloatModel(math) struct { unsigned int G_Ativo :1, G_Tratado :1; float G_Inst_Ativ; } G_E[5]; /*@ requires \valid(&(G_E[0..5-1].G_Ativo)); @ requires \valid(&(G_E[0..5-1].G_Tratado)); @ requires \valid(&(G_E[0..5-1].G_Inst_Ativ)); @*/ void test(int a) { int i = 0; for(i=0;i<5;i++) { if(G_E[i].G_Ativo == FALSE && G_E[i].G_Inst_Ativ <= Tempo) G_E[i].G_Ativo = TRUE; } } 2012/11/12 Virgile Prevosto <virgile.prevosto at m4x.org> > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121113/3cb1bb7b/attachment.html>