--- layout: fc_discuss_archives title: Message 8 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 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