Tidying up the options for goto-instrument #6475
Conversation
This option has long been deprecated and then removed from cbmc. I guess it only stayed in these tests as they have also long been marked as KNOWNBUG.
These are not implemented, not used by any test, removed from other tools and marked deprecated almost 5 years ago.
Note that this is different to --xml-ui which shift the tool's general output into XML; --xml only affects a few options that produce analysis results.
martin-cs
requested review from
chrisr-diffblue,
peterschrammel and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6475 +/- ##
===========================================
+ Coverage 76.02% 76.23% +0.20%
===========================================
Files 1546 1546
Lines 165352 165351 -1
===========================================
+ Hits 125711 126051 +340
+ Misses 39641 39300 -341
Continue to review full report at Codecov.
|
|
Please can someone who understands CTest and the build on Mac help me with this: https://github.com/diffblue/cbmc/runs/4314110590?check_suite_focus=true#step:11:4571 It looks like the |
|
Is it possible to access the |
martin-cs
force-pushed
the
tidy/goto-instrument-options
branch
from
8d8714a to
a46064d
Compare
This also adds: --read-first --write-first --no-loop-duplication --hide-internals which are handled by goto-instrument but were not options so couldn't be used.
This was tested for but does not appear as an option in goto_diff_parse_options.h as a valid option so this code can never be used. Worse, goto-diff doesn't include any of the code that uses it, nor can I think what the memory model might have to do with diffing goto-programs.
martin-cs
force-pushed
the
tidy/goto-instrument-options
branch
from
a46064d to
b71a830
Compare
|
Weirdly, running it again got me an error message. I guess there is something fragile about how CTest is set up? |
|
Hi @martin-cs , looks like everything is passing now. Next time, if you need any help with a mac build feel free to ping me directly - I have access to an intel machine and an m1 machine if that helps. |
| @@ -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" | |||
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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?
I'm working through the options of
goto-instrumentseeing:OPT_andHELP_macros?This is the first handful of these. It is best to review commit by commit as each one is short and mostly separate.
Let me know if you think its worth me doing more of these!