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

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                    |