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
- Subject: [Frama-c-discuss] Jessie - pointer dereferencing
- From: Claude.Marche at inria.fr (Claude Marché)
- Date: Mon, 15 Apr 2013 09:16:36 +0200
- In-reply-to: <CAEtoXR3A8EmQ3MK2iTRmpzmqrnFDMRdgB1VoNzUx3pUgmXbwOw@mail.gmail.com>
- References: <CAEtoXR3A8EmQ3MK2iTRmpzmqrnFDMRdgB1VoNzUx3pUgmXbwOw@mail.gmail.com>
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 |
- Follow-Ups:
- [Frama-c-discuss] Jessie - pointer dereferencing
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] Jessie - pointer dereferencing
- References:
- [Frama-c-discuss] Jessie - pointer dereferencing
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] Jessie - pointer dereferencing
- Prev by Date: [Frama-c-discuss] floating-point examples
- Next by Date: [Frama-c-discuss] floating-point examples
- Previous by thread: [Frama-c-discuss] Jessie - pointer dereferencing
- Next by thread: [Frama-c-discuss] Jessie - pointer dereferencing
- Index(es):