--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on April 2013 ---
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