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