Document all {goto-,j}analyzer options #6929
Conversation
tautschnig
commented
Jun 14, 2022
tautschnig
commented
- Each commit message has a non-empty body, explaining why the change was made.
- n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
It likely never was supported in goto-analyzer and janalyzer, see a35731b for when it was removed from tools that actually supported it.
This commit completes the --help output of the data-flow analysis tools.
tautschnig
requested review from
romainbrenguier,
martin-cs and
chris-ryder
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6929 +/- ##
===========================================
- Coverage 77.79% 77.79% -0.01%
===========================================
Files 1568 1568
Lines 180316 180317 +1
===========================================
Hits 140285 140285
- Misses 40031 40032 +1
Continue to review full report at Codecov.
|
| @@ -757,8 +759,9 @@ void janalyzer_parse_optionst::help() | |||
| "\n" | |||
| "Domain options:\n" | |||
| " --constants constant domain\n" | |||
| " --intervals interval domain\n" | |||
| " --non-null non-null domain\n" | |||
| " --intervals, --show-intervals\n" | |||
There was a problem hiding this comment.
💡 Looks as if there should be a common definition of these options somewhere. Non-blocking.
There was a problem hiding this comment.
Ack, but actually there's quite a lot more that seems to be duplicated across goto-analyzer and janalyzer. A variant of goto-checker would be nice :-) So I'll leave this as-is for now, but will put it in my backlog.
There was a problem hiding this comment.
A. There is a lot that could be refactored between the two. I guess I hadn't because of concern about breaking out-of-tree janalyzer patches. But, yeah, could look at that post-marking.
B. The --show-* options are legacy. The goal is to "orthogonalize" the options so it is --show --intervals. I would rather these were removed (along with their complex option parsing) than documented.
| @@ -757,8 +759,9 @@ void janalyzer_parse_optionst::help() | |||
| "\n" | |||
| "Domain options:\n" | |||
| " --constants constant domain\n" | |||
| " --intervals interval domain\n" | |||
| " --non-null non-null domain\n" | |||
| " --intervals, --show-intervals\n" | |||
There was a problem hiding this comment.
A. There is a lot that could be refactored between the two. I guess I hadn't because of concern about breaking out-of-tree janalyzer patches. But, yeah, could look at that post-marking.
B. The --show-* options are legacy. The goal is to "orthogonalize" the options so it is --show --intervals. I would rather these were removed (along with their complex option parsing) than documented.
|
I've removed the two --show-* options in #6932 (there's still --show-taint and --show-local-may-alias for these appear to be handled differently). |
|
@tautschnig Thank you! |
