/// @noreturn
int foo(double age, char *name);