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

I was thinking about the answer and I did some tests.


1) I have changed the static variable i to global.


2) After, I have tried to use the annotations suggested below:

/*@
predicate invar{L}() =
G_E[0].G_Tratado != 0 ==> 0 <= i <= 2;
*/

/*@ requires invar();
@ ensures invar();
@*/

But it has not run. I think that is because either the variables are global
or it is the Jessie verion (Carbon). The message that was shown:

xxx.c:16:[kernel] user error: unexpected token ')'


2) So, I have decided to write those annotations without predicate :

/*@ requires G_E[0].G_Tratado != 0 ==> 0 <= i <= 2;
@ ensures    G_E[0].G_Tratado != 0 ==> 0 <= i <= 2;
@*/

But it has not worked. I have obtained 2 Vcs not proved related to:
- integer_of_uint8(i) <= offset_max(float_P_acel_2_alloc_table, acel)
- integer_of_int32(resul1) + 1 <=255



3) Some observations about the code.

I am sure that this if statement will occur in the first time that the
function is called. So, the variable i is initialized with 0.
Thank you for explanation about the initialization in the C standard.

  // This if statement is true only in the first time
 if((G_E[0].G_Ativo == 1 && G_E[0].G_Tratado == 0))
     {
       i = 0;
     }

I am sure, that in this point of code i<=2 and i>=0.
 acel[i] = Voo_Acel;

In the next line, the variable i can be become 3 (i=3).
  i = i + 1;

But in the end of function if i>2 it will be become 0 (i=0).
  if (i > 3 - 1)
     {
     i = 0;
     }

The function is not complicated but I does not get prove it.
Actually I am working with a real case study and I can not change the
static variable i to a global variable.

Maybe the results of my verification could indicate that to change the
variable to global would be the best solution but I need
to understand why and the verification should still work.

Does it makes sense to suggest to refactoring the source code? Is my
rationale correct?


5) I have another question.
In the recent my post, I have received the suggestion to use ghost variable
to deal with the problem of static variable.
It has worked. So, I have something like that:

//@ 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;
...
}

But now, I would like to use the annotations written for calc() in the body
function2 such as a contract:

//@ ghost float visible_average;
/*@ ensures (visible_average > 5.0) ==> (G_E[9].G_Ativo == 1);
*/
void calc();

void function2()
{
    calc();
}

But I can not use the visible_average variable in this case. How can I do
this?


Thanks a lot!
Best regards,
Rovedy

struct
{
unsigned int G_Ativo :1,
G_Tratado :1;
float G_Inst_Ativ;
} G_E[61];


unsigned char  i;

float Voo_Acel;

/*@ requires (G_E[0].G_Tratado != 0) ==> 0 <= i <= 2;
@ ensures G_E[0].G_Tratado != 0 ==> 0 <= i <= 2;
*/
void calc()
  {
  static          float acel[3];
  static unsigned char  pri;


  // 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;
     }

 acel[i] = Voo_Acel;
  i = i + 1;

  if (i > 3 - 1)
     {
     i = 0;
     pri = 1;
     }
 }



2013/2/19 Claude Marche <Claude.Marche at inria.fr>

>
> 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<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>
>>     <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<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>
>>
>
> --
> 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                    |
>
>
>
> ______________________________**_________________
> 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/20130220/b3b2aed4/attachment.html>