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

[Frama-c-discuss] [Value Analysis] Math functions



Hello,

We are verifying a flight control software using the Value Analysis plugin
(Carbon version).
It employs some math functions as fabs() and cos().

We have implemented a fabs function that combined with the if statement
resulted in a wrong value as can be checked in the Cvo_Xa2 variable.
However, if the fabs function and the if statement were used separately we
have a correct result as in the Cvo_Xa1 variable.

A similar behaviour happens with the cos function. If several cos function
calls are combined in the same expression a wrong result is obtained as can
be checked in the result2 variable. However, if the cos function is called
and assigned to variables in a separately way, the result is correct as in
the result1 variable.

We have figured out that the expressions using math functions must be kept
as simpler as possible to the Frama-C give the more precise range of the
variables.

Is there an explanation about this behaviour?

We ran the following line command and part of the log file is shown bellow

frama-c -val fabssin.c /usr/share/frama-c/builtin.c
/usr/share/frama-c/math.c

[value] ====== VALUES COMPUTED ======
[value] Values for function fabs2:
[value] Values for function computeFABS:
          Cvo_Xa1 ? 1.06590592813e-08
          Cvo_Xa2 ? [0. .. 1.06590592813e-08]
          Beta ? 0.000277546582353
          aux ? 0.000277546582353
[value] Values for function cos:
[value] Values for function computeCos:
          Cos_Y ? 1.
          Cos_Z ? 1.
          Y ? {0; }
          Z ? {0; }
          result1 ? 1.
          result2 ? [-2147483648. .. 2147483647.]
[value] Values for function main:
          Cvo_Erro_Atit ? 0.000975589579534
          Cvo_Fqrp ? 0.000749183219486
          Cvo_Py_Interp[0] ? 1.4153537975
                       [1] ? 1.47261418188
                       [2] ? 0.00069924875

Best regards,
Rovedy, Nanci, Luciana

//-------------------------------------------------------------------------------

double fabs2(double x){
  if (x==0.0) return 0.0;
  if (x>0.0) return x;
  return -x;
}

void computeFABS (double Cvo_Erro_Atit,double Cvo_Fqrp, float
Cvo_Py_Interp[])
{
  double Cvo_Xa1, Cvo_Xa2, Beta, aux;

  Cvo_Xa1 = Cvo_Xa2 = 0.0;

  Beta = Cvo_Py_Interp[0] * Cvo_Erro_Atit + Cvo_Xa1 - Cvo_Py_Interp[1] *
Cvo_Fqrp;

  aux = fabs2(Beta);
  if(aux < 5.235988e-2)
     Cvo_Xa1 = Cvo_Xa1 + Cvo_Py_Interp[2] * 0.015625 * Cvo_Erro_Atit;

  if(fabs2(Beta) < 5.235988e-2)
     Cvo_Xa2 = Cvo_Xa2 + Cvo_Py_Interp[2] * 0.015625 * Cvo_Erro_Atit;
}

//-------------------------------------------------------------------------------

void computeCos()
{
float Cos_Y, Cos_Z, Y, Z, result1, result2;
  Y = Z = 0.0;

  Cos_Y = cos(Y);
  Cos_Z = cos(Z);
  result1 = Cos_Z * Cos_Y;
  result2 = cos(Z) * cos(Y);
}

//-------------------------------------------------------------------------------

void main ()
{

  double Cvo_Erro_Atit,Cvo_Fqrp;
  float Cvo_Py_Interp [3];

  Cvo_Erro_Atit = 0.000975589579534;
  Cvo_Py_Interp[0] = 1.4153537975;
  Cvo_Py_Interp[1] = 1.47261418188;
  Cvo_Py_Interp[2] = 0.00069924875;
  Cvo_Fqrp = 0.000749183219486;

  computeFABS(Cvo_Erro_Atit, Cvo_Fqrp, Cvo_Py_Interp);

  computeCos();

}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130422/4cf20247/attachment.html>