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