double ieee_extended_to_double(const unsigned char *);