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

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>