Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Jessie - static variable
- Subject: [Frama-c-discuss] Jessie - static variable
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- Date: Wed, 20 Feb 2013 10:54:07 -0300
- In-reply-to: <5123A3CC.3000501@inria.fr>
- References: <CAEtoXR1pJfHHoWB-0DDMqyO2U-qW3FfuftjxPbeguVeTStUBtQ@mail.gmail.com> <512141F6.2040003@inria.fr> <CAEtoXR1rGXFyAyYNfOq9d3wvay8=pgFL35-9d5JDh9Y60_V6qQ@mail.gmail.com> <5123A3CC.3000501@inria.fr>
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>
- References:
- [Frama-c-discuss] Jessie - static variable
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] Jessie - static variable
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Jessie - static variable
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] Jessie - static variable
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Jessie - static variable
- Prev by Date: [Frama-c-discuss] Jessie - static variable
- Next by Date: [Frama-c-discuss] Jessie - behavior
- Previous by thread: [Frama-c-discuss] Jessie - static variable
- Next by thread: [Frama-c-discuss] Jessie - behavior
- Index(es):