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




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                    |