Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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