--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on February 2013 ---
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; ... }