fix buffer overflow in printf formatting of denormals with low bit set

fix buffer overflow in printf formatting of denormals with low bit set

empirically the overflow was an off-by-one, and it did not seem to be
overwriting meaningful data. rather than simply increasing the buffer
size by one, however, I have attempted to make the size obviously
correct in terms of bounds on the number of iterations for the loops
that fill the buffer. this still results in no more than a negligible
size increase of the buffer on the stack (6-7 32-bit slots) and is a
"safer" fix unless/until somebody wants to do the proof that a smaller
buffer would suffice.