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 - pointer dereferencing

  • Subject: [Frama-c-discuss] Jessie - pointer dereferencing
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Sun, 14 Apr 2013 15:28:31 -0300
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>