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