syst_int64_to_float64
float64 syst_int64_to_float64( int64 );
test_a_int64_z_float64( int64_to_float64, syst_int64_to_float64 );