__floatunditf
long double __floatunditf(u_quad_t);
long double __floatunditf(uint64_t x);
#define uint64_to_float128 __floatunditf