--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on February 2013 ---
Hello, The tip about ghost variable has worked very well. Thank you. Actually, I have never used this kind of annotation and I am learning about Jessie. Now, I have an question about a static variable being used such as index of array. This function is called in a loop, and visually it is possible to see that there is not a problem with the index "i", because when it is equal a 3 it is initialized with 0 (i=0). When I run without annotation, I have obtained 4 Vcs: - offset_min(float_P_acel_2_alloc_table, acel) <=i - i <= offset_max(float_P_acel_2_alloc_table, acel) - offset_min(float_P_acel_2_alloc_table, acel) <=i - i <= offset_max(float_P_acel_2_alloc_table, acel) It seems that the VCs not proved are related with first if statement (i.e. with your no execution). My first attempt was to write an assertion like that: //@ assert (i>=0) && (i<=2); acel[i] = Voo_Acel; i = i + 1; The safety VCs were proved but the assertions VCs not. I thought that if I write an annotation to indicating that the function will run the if statement ( if((G_E[0].G_Ativo == 1 && G_E[0].G_Tratado == 0)) only in the first time it would work. But I didnt get to write this. How can I write this? This solution make sense? Thanks a lot! Best regards, Rovedy #pragma JessieIntegerModel(math) #pragma JessieTerminationPolicy(user) #pragma JessieFloatModel(math) struct { unsigned int G_Ativo :1, G_Tratado :1; float G_Inst_Ativ; } G_E[61]; float Voo_Acel; void calc() { static float acel[3]; static unsigned char pri, i; // This if statement is true only in the first time if((G_E[0].G_Ativo == 1 && G_E[0].G_Tratado == 0)) { pri = 0; i = 0; } //@ assert (i>=0) && (i<=2); acel[i] = Voo_Acel; i = i + 1; if (i > 3 - 1) { i = 0; pri = 1; } } 2013/2/17 Claude Marche <Claude.Marche at inria.fr> > > Hi, > > > > On 02/17/2013 01:35 PM, Rovedy Aparecida Busquim e Silva wrote: > >> 2) After the safety verification, I have tried to do the functional >> verification. I have written a pos-condition that test the static >> variable average like that: >> >> @ ensures (average > 5.0) ==> (G_E[A].G_Ativo == TRUE); >> >> But when I have tried to run, I have received this message: >> xx.c:19:[kernel] user error: unbound logic variable average in annotation. >> >> Is it wrong to use the "average" static variable in a pos-condition? >> > > Yes it is: the post-condition is supposed to be visible to the caller of > your function, but the "average" variable is not visible. > > My simple advice: do not try anything complicated with invariants. Use > ghost variables instead. e.g > > //@ ghost float visible_average; > > /*@ ensures (visible_average > 5.0) ==> (G_E[9].G_Ativo == 1); > */ > void calc() > { > > ... > > > average = add / 3.0; > //@ ghost visible_average = average; > > ... > } > > > > ______________________________**_________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.**inria.fr<Frama-c-discuss at lists.gforge.inria.fr> > http://lists.gforge.inria.fr/**cgi-bin/mailman/listinfo/**frama-c-discuss<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/20130218/af1a04d2/attachment.html>