goto-cc with command line option file

[naiyujiang]

CBMC version: 5.43.0 (cbmc-5.43.0)
Operating system: Linux
Exact command line resulting in the issue: goto-cc @param
What behaviour did you expect: goto-cc @param should produce .gb file
What happened instead: goto-cc @param gives Error opening file '' error

Hi team,

I found that goto-cc is not able to parse command line option file correctly if all options/tokens are on different lines.

For example, if I have a file named as param like this:

-o
file.gb
test.c

Running gcc @param works fine, but goto-cc @param will give Error opening file '' error.

However, if I modify the param file to put all options/flags on the same line:

-o file.gb test.c

or, only put -o and file.gb on the same line:

-o file.gb
test.c

In both cases, goto-cc @param works fine. This seems as a bug if goto-cc is being used as a drop-in replacement of gcc in the build process. I wonder if this is a known issue or work-as-expected?

Thanks!

[tautschnig]

Thank you for your detailed report and the extra debugging already done! This issue will be fixed once #6595 has been merged.