Skip to content

Tidying up the options for goto-instrument #6475

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 14 commits into from
Dec 1, 2021
Merged

Tidying up the options for goto-instrument #6475

Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
96306e4
--all is not implemented, not clear that it has a sensible implementa…
Nov 22, 2021
27d4ab6
OPT_ and HELP_ macros for the document properties flags
Nov 22, 2021
f836466
Add basic "does it run" tests for the --document options
Nov 22, 2021
6a18cb1
OPT_ and HELP_ macros for the dump-c flags
Nov 22, 2021
033506b
Remove --no-pointer-check from CBMC KNOWNBUG tests
Nov 23, 2021
49f44f8
Remove the --no-*-check options from goto-instrument
Nov 23, 2021
62c3062
OPT_ and HELP_ macros for the remove options flag
Nov 23, 2021
75873b5
Document the XML output option
Nov 23, 2021
8c47a4f
OPT_ and HELP_ macros for the uninitialized local variable check flag
Nov 23, 2021
8a6ff17
Improve the error messages given by the uninitialized checks
Nov 23, 2021
44a1fc9
Add a test for the uninitialized local variable check
Nov 23, 2021
6fb3bff
Fix up the include order of local headers
Nov 23, 2021
b1c61dc
OPT_ and HELP_ macros for the weak memory model flags
Nov 24, 2021
b71a830
Remove the --mm option from goto-diff
Nov 24, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/goto-instrument/goto_instrument_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1851,6 +1851,7 @@ void goto_instrument_parse_optionst::help()
"Other options:\n"
" --version show version and exit\n"
HELP_FLUSH
" --xml output files in XML where supported\n"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it possible to add some documentation in the docs/ folder for this? I wasn't aware of the difference between --xml and --xml-ui

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is but...

A. The current state of the goto-instrument documentation ( https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/goto-instrument.md ), apart from function body generation and contracts is pretty abysmal. I do want to improve it but it is after "tidying up, figuring out and testing" the options on my TODO list.

B. I am not sure that it should even be an option or called that. At the moment I am going with preserving functionality but I am also building a set of "I think this would be sensible" changes. As it stands it is a formerly undocumented option that works with only two of the flags. I do wonder if it would make more sense if it followed the same convention as goto-analyzer. Or maybe it would be better to move all of the functionality over to goto-analyzer?

" --xml-ui use XML-formatted output\n"
" --json-ui use JSON-formatted output\n"
HELP_TIMESTAMP
Expand Down