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

[Frama-c-discuss] Value Analysis - iterative function



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>