--- layout: fc_discuss_archives title: Message 28 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 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