--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on May 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plugin



Actually, the structure of the code is the follow:

float beta[4];   // global variable

ComputeValue ()
{
 beta[0]= value x;
 beta[1]= value y;

       limiValue(&beta[0],&beta[1]);
}

If I understood the comment, the variable is the same (array Beta).
But when I look at  the function limitValue I have two pointers distinct.
I couldn?t understand why my behavior specification is invalid.
What should I do?
What is the correct specification for my function?

Thanks,
Rovedy


2012/5/3 Claude Marche <Claude.Marche at inria.fr>

>
> Hi,
>
>  ------------------------------**------------------------------**
>> ------------------------------**-------------------
>> 1) I would like to use behavior specification (see the function below).
>> But I couldn?t prove the Vcs
>> related with the behavior one:
>> I didn't understand the problem. If I don?t use behavior , I have all
>> the proven VCs.
>>
>
>
>> /*@ assigns \nothing;
>>   @ ensures \result == \abs(x);
>> @*/
>> extern double fabs(double x);
>>
>> #define LIMIT 6.111111e-2
>>
>> /*@ requires \valid(AB_Ptr) && \valid(CD_Ptr);
>>
>
> The right question is: are AB_Ptr and CD_ptr separated ? My guess is that
> if you pass the same pointer for both arguments, your contract with
> behaviors does not hold.
>
> - Claude
>
> --
> 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/20120503/6f42c6b9/attachment-0001.html>