lit/Driver/Inputs/hello.c

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

int main(int argc, char **argv) {
  printf("Hello World\n");
  return 0;
}