__fpu_ftox
uint32_t __fpu_ftox(struct fpemu *, struct fpn *, uint32_t *);
space[0] = __fpu_ftox(fe, fp, space);