--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on May 2013 ---
Hi, 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? Best regards, Nanci, Rovedy, Luciana 2013/5/22 Roberto Bagnara <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>> > > > > 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 > > _______________________________________________ > 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 > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130522/96674a69/attachment.html>