--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on August 2011 ---
>> 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. 1) Sorry for my mistake. I am sending the function with the new annotations (2 versions) but the VCs related with ensures clauses aren't proved. /*@ assigns \nothing; @*/ extern double fabs(double) ; #define LIMIT 6.111111e-2 #pragma JessieFloatModel(defensive) /*@ requires \valid(AB_Ptr) && \valid(CD_Ptr); @ assigns *AB_Ptr, *CD_Ptr; @ ensures -6.111111e-2 <= *AB_Ptr <= 6.111111e-2; @ ensures -6.111111e-2 <= *CD_Ptr <= 6.111111e-2; @ */ void limitValue(float *AB_Ptr, float *CD_Ptr) { double Fabs_AB, Fabs_CD; double max; Fabs_AB = fabs (*AB_Ptr); Fabs_CD = fabs (*CD_Ptr); max = Fabs_AB; if (Fabs_CD > Fabs_AB) max = Fabs_CD; if ( max > LIMIT) { *AB_Ptr = (float) (((*AB_Ptr) * LIMIT) / max); *CD_Ptr = (float) (((*CD_Ptr) * LIMIT) / max); } } And another alternative is: /*@ requires \valid(AB_Ptr) && \valid(CD_Ptr); @ assigns *AB_Ptr, *CD_Ptr; @ ensures \abs(*AB_Ptr) <= 6.111111e-2; @ ensures \abs(*CD_Ptr) <= 6.111111e-2; @ */ Neither annotations works. Can you help me? >> 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. 2) I have gotten with this option 7 default behavior and 145 safety Vcs against 669 default behavior and 2725 safety cheking. I think that I will use this option. I'm very grateful for the help Best regards, Rovedy