# 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

**Follow-Ups**:**[Frama-c-discuss] [Value Analysis] Math functions***From:*rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)

**References**:**[Frama-c-discuss] [Value Analysis] Math functions***From:*rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)

- Prev by Date:
**[Frama-c-discuss] [Value Analysis] Math functions** - Next by Date:
**[Frama-c-discuss] New Frama-C version: Fluorine** - Previous by thread:
**[Frama-c-discuss] [Value Analysis] Math functions** - Next by thread:
**[Frama-c-discuss] [Value Analysis] Math functions** - Index(es):