--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on May 2013 ---
Hi there. On 05/21/13 20:47, Rovedy Aparecida Busquim e Silva wrote: > Now, we are sending the complete program. In order to test the > program, we have simplified the code and assigned a constant > interval to the variables AB and CD., What is exactly that you wish to prove? Is it the following (modulo typos)? /*@ ensures *AB >= -BETA_SAT && *AB <= BETA_SAT && *CD >= -BETA_SAT && *CD <= BETA_SAT; */ void Limit (float * AB, float * CD); Kind regards, Roberto > //------------------------------------------------------------------------------- > #define BETA_SAT 2.0 > > void Limit (float * AB, float * CD) > { > double max,Fabs_AB, Fabs_CD; > > Fabs_AB = fabs2 (*AB); > Fabs_CD = fabs2 (*CD); > > max = Fabs_AB; > if (Fabs_CD > Fabs_AB) > max = Fabs_CD; > > if (max > BETA_SAT) > { > *AB = (float) (((*AB) * BETA_SAT) / max); > *CD = (float) (((*CD) * BETA_SAT) / max); > } > > Frama_C_dump_each(); > } > > //------------------------------------------------------------------------- > double fabs2(double x){ > if (x==0.0) return 0.0; > if (x>0.0) return x; > return -x; > } > > //------------------------------------------------------------------------- > void main () > { > float test1, test2; > > test1= Frama_C_float_interval(1.0, 4.0); > test2= Frama_C_float_interval(1.0, 8.0); > > Limit (&test1, &test2); > } > > > > 2013/5/17 Virgile Prevosto <virgile.prevosto at m4x.org <mailto:virgile.prevosto at m4x.org>> > > Hello, > > 2013/5/16 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br <mailto:rovedy at ig.com.br>>: > > We would like to ask you a suggestion about an algorithm in our case study. > > Our case study is complex and it is composed of several functions. > > Almost all of them were correctly verified by Frama-c Value Analysis plugin > > and gave the expected results, except one. > > > > To exemplify the situation, we simplified the program to send to you. > > We calculate some variables (test1 and test2) that must be between a range > > (-BETA_SAT and BETA_SAT). > > The function Limit() checks the bounds and verify which variable has the > > larger absolute value (test2 in our example), > > this variable receives the limit value (BETA_SAT) with the correct signal. > > The other variable (test1 in our example) receives the proportional > > correction. > > > > BETA_SAT is not defined in your code. I guess that it is also an > interval? If this is the case and you have > BETA_SAT=Frama_C_interval(0.,15.) for instance, you indeed have an > issue, because of the lack of relation between max and BETA_SAT. > Somehow, you have to force value to recognize the fact that when > BETA_SAT's magnitude is very small, then so is max, so that the > division is safe. This can be done by splitting the interval for > BETA_SAT, using a disjunction of the form /*@ assert 0<= BETA_SAT < > 0x1p-1074 || 0x1p-1074 <= BETA_SAT < 0x1p-1073 || ... || 0.5 <= > BETA_SAT <1. || 1<= BETA_SAT; */ and an appropriate slevel. Of course, > said disjunction would be generated by a script rather than written by > hand. The number of subdivisions may probably be adapted depending on > precision needs and run time of the analysis. > > Best regards, > -- > E tutto per oggi, a la prossima volta > Virgile > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr> > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Prof. Roberto Bagnara Applied Formal Methods Laboratory - University of Parma, Italy mailto:bagnara at cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara at bugseng.com