--- layout: fc_discuss_archives title: Message 34 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



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                    |