/* used by gcc for switching the FPU between single and double precision */
const unsigned long __fpscr_values[2] = { 0, 0x80000 };