syst_floatx80_to_int32
int32 syst_floatx80_to_int32( floatx80 );
test_a_floatx80_z_int32( floatx80_to_int32, syst_floatx80_to_int32 );