--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on May 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Value Analysis] Interval Division



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>