void DUMP(char *s);