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



Hello,

On 30/11/2011 23:22, Stephen Siegel wrote:
> What is the right way to use floating-point addition in a specification?  For example, I want to say
>
> ensures x == y + z;
>
> where x, y, and z are variables in the program, and I want the "+" to mean "floating-point addition" (i.e., whatever the "+" means inside the program), not "real (mathematical) addition".
>

If I'm not mistaken, addition on floating-point values is defined by 
IEEE754 as rounding the result of the addition on the corresponding real 
number. Thus, your ensures clause could be expressed (assuming x,y and z 
are double and rounding mode is nearest even. The various other 
possibilities are described in ACSL manual, section 2.2.5) as

//@ ensures x == \round_double(\NearestEven,y+z);

NB: the \eq_double function is unimplemented in the current version of 
Frama-C.

Hope this helps,
-- 
E tutto per oggi, a la prossima volta
Virgile