db_dump_fpstate
{ "fpstate", db_dump_fpstate,0, 0 },
void db_dump_fpstate(db_expr_t, int, db_expr_t, char *);