--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on December 2011 ---
Le 01/12/2011 11:11, Virgile Prevosto a ?crit : > 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. Indeed, your anonymous expert is right. But to remain simple, assuming that the user uses the default Jessie mode for analyzing floating-point programs, where it is requires to show non-overflow, the best way to specify x = y+z is //@ ensures x == \round_double(\NearestEven,y+z); With the mode supporting special values, it is probably //@ ensures \eq_float(x,\add_float(y,z)); (!*untested*!, \add_float probably not supported) -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |