--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on December 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] using floating-point + in spec



On 01/12/2011 10:31, Claude Marche wrote:
>
> Yes and no. The function \eq_float is implemented, and I think it
> applies to apply both on type float and double. The ACSL document may be
> unaccurate on this point.

Point taken. \eq_float is indeed overloaded to take into account both 
float and double in Frama-C (and the ACSL document is inaccurate on this 
point ;-).

> Anyway, for me it is not related to the original question, since the
> purpose of \eq_float is to support special values (infinities and NaN)

But x (a floating point variable coming directly from C), as well as 
\round_double(\NearestEven,y+z) could namely be infinities. It thus 
makes sense to use \eq_float to compare them.

-- 
E tutto per oggi, a la prossima volta
Virgile