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