--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on February 2013 ---
I feel that using a ghost variable does not help for your variable i. I recommend to make i global, to avoid the technical problems with static local variables. This will not solve your problem: you still have to state a kind of invariant, I feel something like that might work : /*@ predicate invar{L}() = G_E[0].G_Tratado != 0 ==> 0 <= i <= 2; */ /*@ requires invar(); @ ensures invar(); @*/ void calc() { ... Notice that it seems that your code relies on the fact that static variables are initialised to 0. I'm not sure it is guaranteed by the C standard. - Claude Le 18/02/2013 22:59, Rovedy Aparecida Busquim e Silva a ?crit : > 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 > <mailto: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 > <mailto: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> > > > > > _______________________________________________ > 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 -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |