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] Use of Jessie and Value Analysis plug-in
- Subject: [Frama-c-discuss] Use of Jessie and Value Analysis plug-in
- From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
- Date: Fri, 19 Aug 2011 00:15:35 +0200
- In-reply-to: <CAEtoXR2yzkk9sKSa4gy+7hAAQwWNZAZGXDQe+5Py94BS1tcLog@mail.gmail.com>
- References: <CAEtoXR2yzkk9sKSa4gy+7hAAQwWNZAZGXDQe+5Py94BS1tcLog@mail.gmail.com>
Le jeudi 18 ao?t 2011 ? 16:57 -0300, Rovedy Aparecida Busquim e Silva a ?crit : > Jessie 1) I have installed the Alt-Ergo 0.91, Simplify 1.5.4, Yices > 1.0.29, CVC3 2.2., and Gappa 0.15.0. > My first problem was a short function responsible by limiting a value > in an interval ?6.111111e-2 to +6.111111e-2 > I created the annotation below but I didn?t get prove. The code is > showed below. I don?t know what I am doing wrong. > > /*@ requires \valid(AB) && \valid(CD); > @ assigns *AB_Ptr, *CD_Ptr; > @ ensures \abs(-6.111111e-2) <= *AB <= \abs(6.111111e-2); > @ ensures \abs(-6.111111e-2) <= *CD <= \abs(6.111111e-2); > @ */ Note that you are trying to prove that *AB and *CD are exactly equal to 6.111111e-2, which is always false! So it's a good thing you were not able to prove it. Get rid of the \abs expressions. > Jessie 2) in another function, with a high number of computations (12 > ifs, 28 assignments, 1 loop, 21 pointers accesses.) > The Jessie generated 2725 VCs for the safety checking. Is it normal? > It is appropriate to evaluate this function with Jessie? (Because the > computer is not a god machine I checked only one part #264). The following option might help you: frama-c -jessie -jessie-why-opt=--fast-wp <file.c> VCs won't get simpler and more easily provable, but at least there should be less of them. Best regards, Guillaume
- Follow-Ups:
- [Frama-c-discuss] Use of Jessie and Value Analysis plug-in
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] Use of Jessie and Value Analysis plug-in
- References:
- [Frama-c-discuss] Use of Jessie and Value Analysis plug-in
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] Use of Jessie and Value Analysis plug-in
- Prev by Date: [Frama-c-discuss] Use of Jessie and Value Analysis plug-in
- Next by Date: [Frama-c-discuss] Use of Jessie and Value Analysis plug-in
- Previous by thread: [Frama-c-discuss] Use of Jessie and Value Analysis plug-in
- Next by thread: [Frama-c-discuss] Use of Jessie and Value Analysis plug-in
- Index(es):