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: Tue, 23 Apr 2013 14:01:29 -0300
  • In-reply-to: <7fy5c9d5y2.fsf@cea.fr>
  • References: <CAEtoXR0C=CRVevFGB=sRAcH7u66x1seaZHOAnL0bqLoNWdA6sA@mail.gmail.com> <7fy5c9d5y2.fsf@cea.fr>
Hi Matthieu,

Thank you for your answer that helped us to understand how the plugin works.

Yes, you are right, the results were only imprecise, but not wrong.

However, in one of the scenarios from our case study, we need the exact
values and not the intervals.

We intend to update to the new version of Frama-C.

Best regards
Nanci, Rovedy, Luciana


2013/4/23 Matthieu Lemerre <matthieu.lemerre at cea.fr>

>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130423/b438590a/attachment.html>