--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on May 2012 ---
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>