--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on February 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie - static variable



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                    |