incorrect rounding of hexadecimal, octal numbers in gawk 3.1.3

[Paul Eggert]

The hexadecimal value 0x200000000000011 cannot be represented exactly
as a gawk number, so gawk rounds it.  Unfortunately, gawk rounds it
incorrectly, to 144115188075855872 (an error of 17).  The nearest gawk
number is 144115188075855904 (an error of 15).  There is a similar
problem with octal values.

Here is a shell transcript illustrating the problem on a Solaris 8
(sparc) platform.

  $ gawk 'BEGIN {printf "%d %d %d\n", 144115188075855889, 
010000000000000000021, 0x200000000000011}' </dev/null
  144115188075855904 144115188075855872 144115188075855872

144115188075855889, 010000000000000000021, and 0x200000000000011 are
all the same number.  Gawk rounds the decimal representation
correctly, but it rounds the octal and hexadecimal representations
incorrectly.

Internally, gawk uses strtod to convert the decimal number, but uses
its own code to convert the hexadecimal number.  I suppose gawk could
use strtod to convert the hexadecimal number itself.  That would be
an improvement, but gawk still wouldn't round octal numbers correctly.