--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on November 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] using floating-point + in spec



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".

Thx,
Steve