extern int printf(char *format, ...);