float32_t __int64_to_float32(int64_t arg);
__int64_to_float32 converts the 64-bit signed integer arg to a 32-bit floating value, rounding if required, and returns the appropriately rounded value as the result.