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

  • Subject: [Frama-c-discuss] [Value Analysis] Interval Division
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Thu, 16 May 2013 16:42:46 -0300
  • In-reply-to: <7fip2k8lb5.fsf@cea.fr>
  • References: <CAEtoXR0w=gbNW5eYiEfEyXNmFPSq1vP_jDf_sDYYuix8pSQgDA@mail.gmail.com> <7fip2k8lb5.fsf@cea.fr>
We would like to thank you for your reply.

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.

This algorithm works correctly with variables with a single value, but it
does not work with intervals,
because of the operations with the intervals including the division.
To deal with this problem we alterated the algorithm to simply limit the
two variables.
However we would like to keep the idea of algorithm, i.e, limit the
variables keeping the proportion between them.

Is that possible? Do you have a suggestion to implement this?

Best regards,
Nanci Naomi, Rovedy, Luciana

void Limit (float * AB, float * CD)
{
   double Fabs_AB, Fabs_CD;
   double max;

   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);
   }
}
//-------------------------------------------------------------------------
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(-10.0, 10.0);
   test2= Frama_C_float_interval(-20.0, 20.0);

   Limit (&test1, &test2);
}




2013/5/15 Matthieu Lemerre <matthieu.lemerre at cea.fr>

>
> Hi,
>
> I think that what you describe is currently not possible with Frama-C
> value analysis. The abstract domains of value consist of numeric
> intervals, which explains your "cartesian product" result.
>
> In the integer case, you managed to get the precise result because the
> assertion you added forced value to perform a case analysis: it tried
> with test1 == 1, then test1 == 2, ... test1 == 5. Of course you cannot
> do that with floats.
>
> What is missing for your analysis are relational domains; in you case,
> just remembering that test1 == test1 would be sufficient to get the most
> precise result. For more complex programs, more complex relational
> domains have to be used.
>
> Another way to improve the precision of the analysis for floats would be
> to perform case analysis using "small" intervals of floats.
>
> Both approaches require new development in Frama-C; if you need them,
> feel free to contact us for a support contract to implement them in
> Frama-C.
>
> Best regards
> Matthieu
>
>
> Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br> writes:
>
> > Hi,
> >
> > We have a doubt.
> > We have a algorithm with some calculations in a loop and there is a
> > division between 2 variables that are intervals. We would like that the
> > result was 1 to variables with the same intervals, i.e., that the Frama-C
> > not compute the cartesian product. How to do that?
> >
> > We ran some examples. In the example 1 with integer variables, it was
> easy
> > to employ asserts and get the correct results.
> >
> > However the problem is with float variables. In the example 2, we have
> > tried to use similar asserts to example 1, but it did not work.
> >
> > In the loop iterations of the algorithm, we are taking in account that:
> > -the intervals values are not constant
> > -the interval range can be large, the minimum value can be negative
> >
> > example 1:
> >
> > int test1, test2;
> > test1= Frama_C_interval(1, 5);
> > aux=(float)test1/(float)test1;
> >
> > Frama-C output of example 1:
> > [value] Values for function main:
> >           aux ? [0.2 .. 5.]
> >           test1 ? {1; 2; 3; 4; 5; }
> >
> > using the following assert in the example 1
> > //@ assert test1 > 0 &&  test1 < 2 || test1 > 1 &&  test1 < 3 || test1 >
> 2
> > && test1 < 4 || test1 > 3 && test1 < 5;
> >
> > Frama-C output of example 1 with assert:
> > [value] Values for function main:
> >           aux ? 1.
> >           test1 ? {1; 2; 3; 4; }
> >
> > example 2:
> > float test1, test2;
> > float aux;
> > test1= Frama_C_float_interval(1.0, 5.0);
> > aux=test1/test1;
> >
> > Frama-C output of example 2:
> > [value] Values for function main:
> >           test1 ? [1. .. 5.]
> >           aux ? [0.2 .. 5.]
> >
> > Thanks a lot.
> > Rovedy, Nanci, Luciana
> > _______________________________________________
> > 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/20130516/c0f7e5a0/attachment.html>