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

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



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>