--- layout: fc_discuss_archives title: Message 18 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



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;

    ...
   }