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 plugin
- Subject: [Frama-c-discuss] Jessie plugin
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- Date: Thu, 3 May 2012 16:59:43 -0300
- In-reply-to: <4FA274EC.3040807@inria.fr>
- References: <CAEtoXR1wZO6+KMH4kGS-iUBr1PoDjQpY2rtXaU5uA+ARC2BKLQ@mail.gmail.com> <4FA274EC.3040807@inria.fr>
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>
- References:
- [Frama-c-discuss] Jessie plugin
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] Jessie plugin
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Jessie plugin
- Prev by Date: [Frama-c-discuss] Jessie plugin
- Next by Date: [Frama-c-discuss] Valid physical address
- Previous by thread: [Frama-c-discuss] Jessie plugin
- Next by thread: [Frama-c-discuss] Jessie plugin
- Index(es):