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