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] Math functions

  • Subject: [Frama-c-discuss] [Value Analysis] Math functions
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Mon, 22 Apr 2013 14:19:42 -0300
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>