--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on December 2011 ---
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