--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on April 2013 ---
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>