int printf(char* format, ...); int gi = 42; int main() { printf("hello world %d\n", gi); }