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

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