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

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>