extern FILE *stdin;
extern FILE *stdout;
extern FILE *stderr;

int fprintf(FILE *restrict stream, const char *restrict format, ...);
int sprintf(char *restrict str, const char *restrict format, ...);
