--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie - pointer dereferencing



Hello,

I have a function that is called two times, each time with different
parameters:

   // The parameters are : I_PY1=0 and float Cvo_Py_Interp [3];
   Interp (I_PY1, Cvo_Py_Interp);
   // The parameters are : I_R1=1 and   float Cvo_R1_Interp [2];
    Interp (I_R1, Cvo_R1_Interp);

And I have a Cvo_Tab_1s_Ptr   array that,in another function,receives the
address for the other arrays:
    Cvo_Tab_1s_Ptr[I_PY1] = Py1[0];
    Cvo_Tab_1s_Ptr[I_R1] =  R1[0];

I have tried to use behaviors for representing the behavior in each call.
However, I have got VCs not proved with the pointer dereferencing in this
line from for loop:
 Cvo_Interp[J] = *(Cvo_Tab_1s_Ptr[Cvo_Itab] + J);

I thought that the lines below could work to prove the validity the pointer
inside the for loop:
    @ requires \valid(Cvo_Tab_1s_Ptr[0] + 0) &&
 \valid(Cvo_Tab_1s_Ptr[0]+1) && \valid(Cvo_Tab_1s_Ptr[0]+2);
    @ requires \valid(Cvo_Tab_1s_Ptr[1] + 0) && \valid(Cvo_Tab_1s_Ptr[1]+1)
&& \valid(Cvo_Tab_1s_Ptr[1]+2);

I dont get to see where my annotation is wrong.
Could someone help me?

Thansk a lot.

Rovedy
*/
//------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

#define PY_QTDCOL 3
#define R1_QTDCOL 2
#define I_PY1   0
#define I_R1    1

float * Cvo_Tab_1s_Ptr [2];

#pragma JessieIntegerModel(math)
#pragma JessieTerminationPolicy(user)
#pragma JessieFloatModel(math)

/*@ requires Cvo_Itab==I_PY1 || Cvo_Itab ==I_R1;
  @ behavior one:
     @ assumes Cvo_Itab == I_PY1;
     @ requires \valid(Cvo_Tab_1s_Ptr[0] + 0) &&
 \valid(Cvo_Tab_1s_Ptr[0]+1) && \valid(Cvo_Tab_1s_Ptr[0]+2);
     @ requires \valid(Cvo_Interp+ (0..3-1));
  @ behavior two:
     @ assumes Cvo_Itab == I_R1;
     @ requires \valid(Cvo_Tab_1s_Ptr[1] + 0) &&
\valid(Cvo_Tab_1s_Ptr[1]+1) && \valid(Cvo_Tab_1s_Ptr[1]+2);
     @ requires \valid(Cvo_Interp+ (0..3-1));
*/
void Interp(unsigned char Cvo_Itab,float Cvo_Interp[])
{
   unsigned char Qtdcol, J;

   Qtdcol = PY_QTDCOL;
   if (Cvo_Itab == I_R1)
      Qtdcol = R1_QTDCOL;

  //@ loop invariant 0<= J && J <= Qtdcol;
    for (J = 0; J < Qtdcol; J++)
 Cvo_Interp[J] = *(Cvo_Tab_1s_Ptr[Cvo_Itab] + J);
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130414/fc103201/attachment.html>