Clean-up and document goto_trace.h/cpp [DOC-136] #4075
Conversation
goto-programs implementation should be language independent, so there is no reason to include a mode field.
This is unused and doesn't bring much compared to the standard erase function.
This is only an intermediary function used by show_goto_trace. It shouldn't be exposed in the interface.
The second version of show_goto_trace was just calling the other one with a default value for the last argument. We do now that explicitly in the signature and remove the need for a second function.
romainbrenguier
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
src/goto-programs/goto_trace.h
Outdated
| /// Step of the trace of a GOTO program | ||
| /// | ||
| /// A step is either: | ||
| /// - an assignement |
There was a problem hiding this comment.
| /// - an assignement | |
| /// - an assignment |
src/goto-programs/goto_trace.h
Outdated
| bool show_function_calls; | ||
| /// how original code in plain trace |
There was a problem hiding this comment.
Show
Maybe: in plain text trace
romainbrenguier
force-pushed
the
doc/symex_trace
branch
2 times, most recently
from
20638d7 to
0c7e8d8
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 20638d7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99755367
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 0c7e8d8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99756516
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
Add documentation to the main classes, functions and methods when their meaning is not obvious.
Doxygen comments should start with ///
romainbrenguier
force-pushed
the
doc/symex_trace
branch
from
c59c8dc to
b88944d
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: b88944d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99764171
No functional changes: only removing unused code and documenting.