dbl_fadd
int dbl_fadd(dbl_floating_point *, dbl_floating_point*, dbl_floating_point*, unsigned int *);
return(dbl_fadd(&fpregs[r1],&fpregs[r2],
return(dbl_fadd(&fpregs[r1],&fpregs[r2],
if (dbl_fadd(&fpregs[ta], &fpregs[ra], (unsigned *) &atmp,