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 - iterative function

  • Subject: [Frama-c-discuss] Value Analysis - iterative function
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Fri, 15 Mar 2013 10:10:54 -0300
Hello,

We are implementing a filter that is used in a flight control software.
The filter algorithm is implemented as a iterative process whose next
iteration is calculated based on the previous calculated value. In that
process, the successive calculations with the Cvo_Xf and Cvo_Fqrp variables
imply accumulated values that grow until reaching the maximum value of the
double variable.

Is there an annotation or a command line option to deal with this type of
iterative algorithm?
It is noticed that using a single value instead of an interval, the
algorithm works well.

We ran the following line command and some parts of the log file is shown
bellow
>> frama-c -val filter.c /usr/share/frama-c/builtin.c -slevel 3840 > log.txt

        Cvo_Fqrp ??? [-0.441164442315 .. 0.439403377322]
        Cvo_Xf[0] ??? {0; }
              [1] ??? [-0.441164442315 .. 0.439403377322]
...
        Cvo_Fqrp ??? [-1.72477568729 .. 1.72394440298]
        Cvo_Xf[0] ??? [-0.441164442315 .. 0.439403377322]
              [1] ??? [-0.968026842207 .. 0.964162618303]
...
        Cvo_Fqrp ??? [-3.8465662583 .. 3.84574818041]
        Cvo_Xf[0] ??? [-0.968026842207 .. 0.964162618303]
              [1] ??? [-1.75390847835 .. 1.7481604756]
...
          Cvo_Fqrp ??? [-1.79769313486e+308 .. 1.79769313486e+308]
          Cvo_Xf[0..1] ??? [-1.79769313486e+308 .. 1.79769313486e+308]
          Xfaux ??? [-1.79769313486e+308 .. 1.79769313486e+308]

Best regards,
Nanci, Rovedy and Luciana

double Cvo_Fqrp;
double Cvo_Xf [2];
double a;
double F_Kf = 6.306410E-1;
double F_A1 = -1.194254E+0;
double F_A2 = 3.565610E-1;
double F_B1 = -1.722219E+0;
double F_B2 = 9.795862E-1;

void main ()
{
double msiARF;
int i;

  Cvo_Xf[0] = 0.0;
  Cvo_Xf[1] = 0.0;

  msiARF = Frama_C_float_interval(-0.699549255939, 0.696756755939);

  for ( i =0; i<3840; i++)
  {
     a=msiARF;
     filter();
     Frama_C_dump_each();
  }
}

void filter ()
{
   double Xfaux;

   Cvo_Fqrp = a;

   Xfaux = F_Kf * Cvo_Fqrp - F_A2 * Cvo_Xf[0] - F_A1 * Cvo_Xf[1];
   Cvo_Fqrp = Xfaux + F_B2 * Cvo_Xf[0] + F_B1 * Cvo_Xf[1];
   Cvo_Xf[0] = Cvo_Xf[1];
   Cvo_Xf[1] = Xfaux;

   Frama_C_show_each_Cvo_Fqrp_I_(Cvo_Fqrp);
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130315/534891d5/attachment.html>