Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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