Are multiplication and division of double exactly defined under C99with __STDC_IEC_559__ ?

[Francois Grieu]

Assume a conforming C99 implementation that defines __STDC_IEC_559__.
Unless I err, "double" is a floating point type capable of exactly
representing all integers in the range [0..0x1FFFFFFFFFFFFF] (that's 53
bit). Also assume FE_TONEAREST is in effect.

Can it be said that multiplication and division of double are exactly
defined? Or/and that the result of the following functions is fully
specified when x and y are in range [0..0x1FFFFFFFFFFFFF]?


typedef unsigned long long tu53;

tu53 mym(tu53 x, tu53 y)
{ return ( x * 1p-53 ) * y ; }

tu53 myd(tu53 x, tu53 y)
{ return y > x ? ( x * 1p53 ) / y : 0; }


TIA,

Francois Grieu