--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on December 2011 ---
On 01/12/2011 11:02, Virgile Prevosto wrote: > 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. > Oops, I forgot something: an anonymous floating-point expert points me to the fact that y and z could themselves be infinity or even NaN. In that case, we are not able to say anything about their sum (As per ACSL manual, we are in fact not able to say anything about their counterpart in the real numbers). Thus I guess that the approach of rounding the result of the addition on reals only works if y and z are neither infinity nor NaN. -- E tutto per oggi, a la prossima volta Virgile