DEFAULT_OUTPUT_FILE
#ifndef DEFAULT_OUTPUT_FILE
The default output filename is \"%s\".\n" ,name, DEFAULT_OUTPUT_FILE);
const char *outfile = DEFAULT_OUTPUT_FILE;