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

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