--no-standard-checks is included in goto-instrument help, but can only be parsed by cbmc and goto-analyzer

[polgreen]

CBMC version: 6.4.1 (cbmc-6.4.1-66-g1e99418017)
Operating system: MacOS Sonoma

Exact command line resulting in the issue:

goto-instrument --no-standard-checks gotobinary1.gb gotobinary2.gb

What behaviour did you expect:

goto instrument should accept the command line argument and not instrument the binary with standard checks. Or the goto-instrument help should not include this option.

What happened instead:

goto-instrument prints a helpfile that includes "--no-standard-checks" as a valid option and then says Unknown option: --no-standard-checks

The problem is that this command line option is included in HELP_GOTO_CHECK, which is being imported to the help functions for cbmc, goto-analyzer, goto-diff and goto-instrument.

% git grep HELP_GOTO_CHECK
ansi-c/goto-conversion/goto_check_c.h:#define HELP_GOTO_CHECK \
cbmc/cbmc_parse_options.cpp:    HELP_GOTO_CHECK
goto-analyzer/goto_analyzer_parse_options.cpp:    HELP_GOTO_CHECK
goto-diff/goto_diff_parse_options.cpp:    HELP_GOTO_CHECK
goto-instrument/goto_instrument_parse_options.cpp:    HELP_GOTO_CHECK

But this is only handled by two of the option parsers:

% git grep '"no-standard-checks"'
cbmc/cbmc_parse_options.cpp:    options, !cmdline.isset("no-standard-checks"));
cbmc/cbmc_parse_options.cpp:    cmdline.isset("cover") && !cmdline.isset("no-standard-checks") &&
goto-analyzer/goto_analyzer_parse_options.cpp:    options, !cmdline.isset("no-standard-checks"));