syst_int64_to_floatx80
floatx80 syst_int64_to_floatx80( int64 );
test_a_int64_z_floatx80( int64_to_floatx80, syst_int64_to_floatx80 );