Add description of return removal #4091
Conversation
danpoe
commented
Feb 5, 2019
danpoe
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- 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).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
danpoe
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
| /// The types of function pointer expressions in the goto program are however | ||
| /// not changed. For example, in an assignment where `func` is assigned to a | ||
| /// function pointer, such as `int (*f)(void) = func`, the function types | ||
| /// appearing in the lhs and rhs both retain the integer return type. |
There was a problem hiding this comment.
This paragraph documents the current behavior which should probably be changed at some point. Not sure if there would be any pitfalls with it though.
src/goto-programs/remove_returns.h
Outdated
| /// program. The `restore_returns()` functions restore the returns in a goto | ||
| /// program in which they have been removed previously. | ||
| /// | ||
| /// In a goto program in which returns have not beem removed, functions return |
| /// ``` | ||
| /// | ||
| /// As `return` instructions are removed, the return types of the function types | ||
| /// are set to void as well (represented by the type `empty_typet`). This |
There was a problem hiding this comment.
What's the difference between void_typet and empty_typet ?
There was a problem hiding this comment.
At the moment void_typet is defined as class void_typet:public empty_typet {};. I think use of void_typet is deprecated now.
There was a problem hiding this comment.
Yes, I really think we should get rid of void_typet - we don't use it consistently and effectively rely on empty_typet() == void_typet(). I'll put up a PR.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 36bff33).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99812467
src/goto-programs/remove_returns.cpp
Outdated
| @@ -9,7 +9,7 @@ Date: September 2009 | |||
| \*******************************************************************/ | |||
|
|
|||
| /// \file | |||
| /// Remove function return values | |||
| /// Remove function returns | |||
There was a problem hiding this comment.
Maybe "Replace function returns by assignments to global variables"
src/goto-programs/remove_returns.h
Outdated
| /// r = func(); | ||
| /// ``` | ||
| /// | ||
| /// The return removal pass introduces a global variable `func#return_value` |
There was a problem hiding this comment.
thread-local global variable
| /// ``` | ||
| /// | ||
| /// As `return` instructions are removed, the return types of the function types | ||
| /// are set to void as well (represented by the type `empty_typet`). This |
There was a problem hiding this comment.
Yes, I really think we should get rid of void_typet - we don't use it consistently and effectively rely on empty_typet() == void_typet(). I'll put up a PR.
danpoe
force-pushed
the
doc/update-remove-returns-documentation
branch
from
36bff33 to
39b453a
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 39b453a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99918689
