  Current critical systems commonly use a lot of floating-point computations,
and thus the testing or static analysis of programs containing floating-point
operators has become a priority. However, correctly defining the semantics of
common implementations of floating-point is tricky, because semantics may
change with many factors beyond source-code level, such as choices made by
compilers. We here give concrete examples of problems that can appear and
solutions to implement in analysis software.
