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


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                    |