syst_int32_to_floatx80
floatx80 syst_int32_to_floatx80( int32 );
test_a_int32_z_floatx80( int32_to_floatx80, syst_int32_to_floatx80 );