Yet another superfluous buffering layer.  input_file was using FILE*,
but we're better off with unbuffered I/O using open(), read(), ...