floatx80_to_float128
float128 floatx80_to_float128( floatx80 ) __dso_protected;
time_a_floatx80_z_float128( floatx80_to_float128 );
float128 floatx80_to_float128( floatx80 );