Synopsis
float64_t __uint64_to_float64(uint64_t arg);
Description

__uint64_to_float64 converts the 64-bit unsigned integer arg to a 64-bit floating value, rounding if required, and returns the appropriately rounded value as the result.