sgl_to_dbl_fcnvxf
int sgl_to_dbl_fcnvxf(int *, dbl_floating_point *, unsigned int *);
return(sgl_to_dbl_fcnvxf(&fpregs[r1],