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

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                    |