--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on August 2011 ---
[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