float64_t __int16_to_float64(int16_t arg);
__int16_to_float64 converts the 16-bit signed integer arg to a 64-bit floating value and returns the floating value as the result. As all 16-bit integers can be represented exactly in 64-bit floating point format, rounding is never necessary.