Improve GOTO programs high-level documentation #3383
Conversation
smowton
requested review from
kroening,
peterschrammel,
pkesseli and
tautschnig
as code owners
| are littered with \ref code_skipt "skip" statements. The | ||
| instrumentation stage removes the majority of these. | ||
| The `codet` representation of method bodies that is stored in the symbol table | ||
| resembles C code quite strongly: it uses lexical variable scoping and has |
There was a problem hiding this comment.
Should this some how refer to the parse tree, saying that codet is the type-checked version of the parse tree and thus uses lexical ...
There was a problem hiding this comment.
That's only true for C though -- Java and other code doesn't necessarily follow that pattern
src/goto-programs/README.md
Outdated
| conversion and driver-program transformation. | ||
|
|
||
| `goto_symext` is able to use such a lazy GOTO model in place of the usual | ||
| `goto_modelt`, enabling it to fault GOTO programs in on demand, and thus avoid |
There was a problem hiding this comment.
With English not being my first language, the use of "fault GOTO programs in" required me to think more than I would expect at this point. Can we find a different way of expressing the on-demand conversion requests?
There was a problem hiding this comment.
changed fault -> create
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 0d71f9b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91196923
src/goto-programs/README.md
Outdated
| structured: all source-file information is converted into a symbol table, then | ||
| each symbol-table method is converted into a GOTO program, then each transform | ||
| is run over the whole GOTO-model in turn. This is fine when the GOTO model | ||
| consumer will use most or all of the results of conversion, but it not then |
src/goto-programs/README.md
Outdated
| spending time and memory generating GOTO programs that symex determines cannot | ||
| in fact be reached. This is particularly useful when the source program contains | ||
| many indirect calls (virtual function calls, or calls via function pointer), as | ||
| the `remove_virtual_funtions` and `remove_function_pointers` passes treat these |
There was a problem hiding this comment.
remove_virtual_functions
smowton
force-pushed
the
smowton/docs/goto-model-creation
branch
2 times, most recently
from
f1f2da1 to
645c11c
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: f1f2da1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91204347
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: 645c11c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91204477
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.
* Clarify that some things described as 'instrumentation' previously were actually part of the normal goto-convert process * Remove duplicate exposition of the `goto_functionst` data structure * Describe the typical post-goto-convert transformations briefly * Describe lazy-goto-modelt
smowton
force-pushed
the
smowton/docs/goto-model-creation
branch
from
645c11c to
008c580
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 008c580).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91222793
of the normal goto-convert process
goto_functionstdata structure