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: matthieu.lemerre at cea.fr (Matthieu Lemerre)
  • Date: Tue, 23 Apr 2013 10:09:09 +0200
  • In-reply-to: <CAEtoXR0C=CRVevFGB=sRAcH7u66x1seaZHOAnL0bqLoNWdA6sA@mail.gmail.com>
  • References: <CAEtoXR0C=CRVevFGB=sRAcH7u66x1seaZHOAnL0bqLoNWdA6sA@mail.gmail.com>
Hello,

> Hello,
>
> We are verifying a flight control software using the Value Analysis plugin
> (Carbon version).

You should note that the Carbon version is 2 years old, and Frama-C has
much improved since then.

> 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.

Actually, the computed interval for Cvo_Xa2 is not wrong, just
imprecise: the correct value is included in
[0. .. 1.06590592813e-08]. So this is a precision issue.

I cannot reproduce this with the latest version of Frama-C (Fluorine). I
suspect that this may be related to the way that temporary variables are
handled in Carbon. In Frama-C the parsing stage normalizes the source
code such that intermediary results, like fabs2(Beta), are saved in
temporary variables. In current Frama-C version it is done like you did
with the "aux" variable,  but maybe that was different in previous
versions, which lead to imprecise results.

> 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.

I cannot reproduce this either; the result is perfectly precise on the
current Frama-C version.

> 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?

In some places the value analysis is able to reduce the interval of
possible values for a variable (e.g. when there is a if or an
assert). But if the variable is temporary, it is currently unable to
propagate the reduction back to the original expression. So writing
simpler code, with named intermediary results, reduces the amount of
temporary variables, and can sometimes make the value analysis more
precise.

Best regards,
Matthieu