On Mon, 18 Dec 2017, I wrote:
... Example: if y = DBL_MIN and x = 2, then y/x underflows to DBL_MIN/2, but the infinite-precision result for atan2(x, y) is slightly larger, so in round-towards-plus-infinity mode the result should never be y/x, but must larger. How much larger? About (y/x)**2/3 times larger.
Er, "must be larger", and "(y/x)**2/3 times y/x larger". The factor is the relative error. It is a tiny fraction of 1 ULP.
This is still far below DBL_MIN, so we don't have to worry about the rounding giving a non-underflowing result. Also the correction is much smaller than 1 double precision ULP, so the correctly rounded result is only 1 ULP higher than y/x. In the default round-to-nearest mode, the correctly rounded result is y/x since y/x is exact and the correction is tiny.
Bruce