--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on February 2013 ---
Hi, I was thinking about the answer and I did some tests. 1) I have changed the static variable i to global. 2) After, I have tried to use the annotations suggested below: /*@ predicate invar{L}() = G_E[0].G_Tratado != 0 ==> 0 <= i <= 2; */ /*@ requires invar(); @ ensures invar(); @*/ But it has not run. I think that is because either the variables are global or it is the Jessie verion (Carbon). The message that was shown: xxx.c:16:[kernel] user error: unexpected token ')' 2) So, I have decided to write those annotations without predicate : /*@ requires G_E[0].G_Tratado != 0 ==> 0 <= i <= 2; @ ensures G_E[0].G_Tratado != 0 ==> 0 <= i <= 2; @*/ But it has not worked. I have obtained 2 Vcs not proved related to: - integer_of_uint8(i) <= offset_max(float_P_acel_2_alloc_table, acel) - integer_of_int32(resul1) + 1 <=255 3) Some observations about the code. I am sure that this if statement will occur in the first time that the function is called. So, the variable i is initialized with 0. Thank you for explanation about the initialization in the C standard. // This if statement is true only in the first time if((G_E[0].G_Ativo == 1 && G_E[0].G_Tratado == 0)) { i = 0; } I am sure, that in this point of code i<=2 and i>=0. acel[i] = Voo_Acel; In the next line, the variable i can be become 3 (i=3). i = i + 1; But in the end of function if i>2 it will be become 0 (i=0). if (i > 3 - 1) { i = 0; } The function is not complicated but I does not get prove it. Actually I am working with a real case study and I can not change the static variable i to a global variable. Maybe the results of my verification could indicate that to change the variable to global would be the best solution but I need to understand why and the verification should still work. Does it makes sense to suggest to refactoring the source code? Is my rationale correct? 5) I have another question. In the recent my post, I have received the suggestion to use ghost variable to deal with the problem of static variable. It has worked. So, I have something like that: //@ 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; ... } But now, I would like to use the annotations written for calc() in the body function2 such as a contract: //@ ghost float visible_average; /*@ ensures (visible_average > 5.0) ==> (G_E[9].G_Ativo == 1); */ void calc(); void function2() { calc(); } But I can not use the visible_average variable in this case. How can I do this? Thanks a lot! Best regards, Rovedy struct { unsigned int G_Ativo :1, G_Tratado :1; float G_Inst_Ativ; } G_E[61]; unsigned char i; float Voo_Acel; /*@ requires (G_E[0].G_Tratado != 0) ==> 0 <= i <= 2; @ ensures G_E[0].G_Tratado != 0 ==> 0 <= i <= 2; */ void calc() { static float acel[3]; static unsigned char pri; // 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; } acel[i] = Voo_Acel; i = i + 1; if (i > 3 - 1) { i = 0; pri = 1; } } 2013/2/19 Claude Marche <Claude.Marche at inria.fr> > > 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<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> >> <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<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> >> > > -- > 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 | > > > > ______________________________**_________________ > 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/20130220/b3b2aed4/attachment.html>