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

I have a function that use static variables (attached file).

In the first step of my verification (safety verification), I have obtained
4 Vcs not proved related to:
- 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)

In the ACSL manual, I have found a example related to the use of a data
invariant on a local static variable.
I am using the Carbon version and it is not possible to prove this example.
void out_char (cha r c) {
 static int col = 0;
//@ global invariant I : 0 <= col <= 79;
 col ++;
 i f ( col >= 80) col = 0;
 }

Browsing in the web, I have found information that Jessie could not prove
this kind of annotation:

http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-December/002920.html



My doubts are:
1) I have read about solutions related to weak and strong invariants. In my
function, I need to study those solutions or there is another simpler
solution?

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?

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;

/*@ ensures  (average > 5.0) ==> (G_E[9].G_Ativo == 1);
 */
void calc()
  {
  static          float average,
                        acel[3],
                        add;
  static unsigned char  pri,
                        i,
                        j;

  if((G_E[7].G_Ativo == 1 && G_E[7].G_Ativo == 0))
  {
     pri = 0;
     i = 0;
     add = 0;
  }

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

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

  if (pri == 1)
  {
         add = 0;
         /*@     loop invariant  0 <= j <= 3 ;        */
         for(j=0;j<3;j++)
            add = add + acel[j];

         average = add / 3.0;

         if(G_E[9].G_Ativo == 0)
              if(average > 5.0)
                 G_E[9].G_Ativo = 1;
  }
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130217/ad091e24/attachment.html>