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



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>

>
> 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<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/20130218/af1a04d2/attachment.html>