--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on April 2013 ---
/* Hi, Thanks a lot for your answer. It works well. However, I have a problem in another for statement the same function. The Cvo_Tab_1s_Ptr contains a address that points to another array whose lenght is [3][3] (actually the size is much bigger). for (J = 0; J < Qtdcol; J ) Valant = *(Cvo_Tab_1s_Ptr[0] (Iant * Qtdcol) J); The tool produces 2 Vcs related to pointer dereferencing. 1) My first idea was to inserting a requires clause to asserting which the addresses pointed by Cvo_Tab_1s_Ptr are valid: @ requires \forall integer i; 0<=i<(MAXLIN_PY1*PY_QTDCOL) ==> \valid(Cvo_Tab_1s_Ptr[0] i); This line dont work, but If I change for the line below, it works: requires \valid(Cvo_Tab_1s_Ptr[0] 0) && \valid(Cvo_Tab_1s_Ptr[0] 1) && \valid(Cvo_Tab_1s_Ptr[0] 2) && \valid(Cvo_Tab_1s_Ptr[0] 3) && \valid(Cvo_Tab_1s_Ptr[0] 4) && \valid(Cvo_Tab_1s_Ptr[0] 5) && \valid(Cvo_Tab_1s_Ptr[0] 6) && \valid(Cvo_Tab_1s_Ptr[0] 7) && \valid(Cvo_Tab_1s_Ptr[0] 8); My problem is that the real size of array is [64][3], so writing the second requires clause seems inappropriated. Is it wrong use requires clause with \forall? What is my mistake with the requires clause using \forall? Thank you. Best regards, Rovedy */ #define PY_QTDCOL 3 #define I_PY1 0 #define MAXLIN_PY1 3 float * Cvo_Tab_1s_Ptr[2]; /*@ requires Cvo_Itab==I_PY1; requires \valid(Cvo_Interp+ (0..3-1)); requires \valid(Cvo_Tab_1s_Ptr+ (0..2-1)); requires \forall integer i; 0<=i<(MAXLIN_PY1*PY_QTDCOL) ==> \valid(Cvo_Tab_1s_Ptr[0] + i); */ void Interp(unsigned char Cvo_Itab,float Cvo_Interp[]) { unsigned char Qtdcol, J, nlin,Iant; float Valant; Qtdcol = PY_QTDCOL; nlin=MAXLIN_PY1; Iant = 2; /*@ loop invariant 0<= J && J <= Qtdcol; loop variant Qtdcol - J; */ for (J = 0; J < Qtdcol; J++) { Valant = *(Cvo_Tab_1s_Ptr[0] + (Iant * Qtdcol) + J); Cvo_Interp[J] = 5.5; } } 2013/4/15 Claude March? <Claude.Marche at inria.fr> > > A requires clause inside a behavior block is not seen as an hypothesis for > the memory accesses in the code, but only a premise of the ensures clauses. > So, put the requires clauses outside the behavior blocks and it will work. > Something like > > > /*@ requires Cvo_Itab==I_PY1 || Cvo_Itab ==I_R1; > @ requires Cvo_Itab==I_PY1 ==> \valid(Cvo_Tab_1s_Ptr[0] + 0) && ... > > > BTW, since you do not have any ensures clauses in your contract, I don't > see any point of having behavior blocks. > > - Claude > > > Le 14/04/2013 20:28, Rovedy Aparecida Busquim e Silva a ?crit : > > >> #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); >> } >> > > -- > 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/20130421/750f2d72/attachment.html>