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


  • Subject: [Frama-c-discuss] using floating-point + in spec
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Thu, 01 Dec 2011 10:31:53 +0100
  • In-reply-to: <4ED73527.8030705@cea.fr>
  • References: <5F048F9B-D8E6-4560-9DEF-38BF8571608D@UDel.Edu> <4ED73527.8030705@cea.fr>

I was about to answer to this question but Virgile did it just before me.

A few additional remarks

On 01/12/2011 09:04, Virgile Prevosto wrote:
> 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);


Yes. And of course you should be aware that this assumes that the 
rounding mode is nearestEven. I think it is good that it is has to be 
made explicit.

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

Yes and no. The function \eq_float is implemented, and I think it 
applies to apply both on type float and double. The ACSL document may be 
unaccurate on this point.

Anyway, for me it is not related to the original question, since the 
purpose of \eq_float is to support special values (infinities and NaN)

- Claude