syst_float64_to_float128
float128 syst_float64_to_float128( float64 );
float64_to_float128, syst_float64_to_float128 );