float128_to_float32
float32 float128_to_float32( float128 ) __dso_protected;
time_a_float128_z_float32( float128_to_float32 );
float32 float128_to_float32( float128 );