--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on December 2011 ---
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