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