--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on May 2013 ---
Thank you for your answer. However, we do not intend to apply other tool, because our project is focused in the Value Analysis plugin/Frama-c. Perhaps, in future works, we would apply some symbolic model checker. Best regards, Nanci, Rovedy, Luciana ---------- Forwarded message ---------- From: Roberto Bagnara <bagnara at cs.unipr.it> Date: 2013/5/25 Subject: Re: [Frama-c-discuss] [Value Analysis] Interval Division To: Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br> Cc: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> On 05/22/13 14:29, Rovedy Aparecida Busquim e Silva wrote: > Yes, we would like to obtain as a result *AB >= -BETA_SAT && *AB <= BETA_SAT && *CD >= -BETA_SAT && *CD <= BETA_SAT. > > In a simplified example with the following inputs: > #DEFINE BETA_SAT 2 > > *AB = 4.0; > *CD = 8.0; > > we obtain the following outputs: > max = 8.0; > > *AB = 4.0 / 8.0 * 2.0 = 1.0; > *CD = 8.0 / 8.0 * 2.0 = 2.0; > > We would like to obtain a similar result in Value Analysis taking in > account input intervals to the variables AB and CD. The expected > result would be AB and CD as output bounded interval by BETA_SAT. Is > that possible? Generally speaking, it is possible (for instance, the property can be easily proved by ECLAIR's symbolic model checker). I don'w know if this is feasible with the current version of Frama-C: if you find out, please let me know. Kind regards, Roberto > 2013/5/22 Roberto Bagnara <bagnara at cs.unipr.it <mailto:bagnara at cs.unipr.it >> > > > 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> <mailto: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> <mailto: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> <mailto: 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 <mailto: 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 <mailto:bagnara at cs.unipr.it> > BUGSENG srl - http://bugseng.com > mailto:roberto.bagnara at bugseng.com<mailto: roberto.bagnara at bugseng.com> > > _______________________________________________ > 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130528/c538c1b1/attachment-0001.html>