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



/* 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>