Move make_allocate_code utility function #4349
Conversation
antlechner
requested review from
cesaro,
cristina-david,
kroening,
NathanJPhillips,
peterschrammel,
pkesseli,
smowton,
tautschnig and
thk123
as code owners
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: f80e3b1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103584559
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.
src/util/allocate_objects.cpp
Outdated
| @@ -271,3 +271,15 @@ void allocate_objectst::mark_created_symbols_as_input(code_blockt &init_code) | |||
| init_code.add(std::move(input_code)); | |||
| } | |||
| } | |||
|
|
|||
| /// Create code allocating object of size `size` and assigning it to `lhs` | |||
There was a problem hiding this comment.
Done in a new "Tidy up documentation" commit. 🐚
src/util/allocate_objects.cpp
Outdated
| { | ||
| side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location()); | ||
| alloc.add_to_operands(size); | ||
| alloc.add_to_operands(false_exprt()); |
There was a problem hiding this comment.
Nowadays you can actually do
side_effect_exprt alloc{ID_allocate, {size, false_exprt()}, lhs.type(), lhs.source_location()};
There was a problem hiding this comment.
Thanks, didn't know about this constructor, I changed it to your suggestion.
| side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location()); | ||
| alloc.add_to_operands(size); | ||
| alloc.add_to_operands(false_exprt()); | ||
| return code_assignt(lhs, alloc); |
There was a problem hiding this comment.
I'd do return code_assignt{lhs, std::move(alloc)};
There was a problem hiding this comment.
Why? Wouldn't return-value optimisation take care of this?
There was a problem hiding this comment.
AFAIK not, because it's a named object. (But also it won't make any difference until #3502 is merged, and even then it will not make a measurable difference.)
There was a problem hiding this comment.
I see, so the pass-by-value constructor for code_assignt doesn't exist yet but hopefully will in the future, when your PR is merged. In that case I'll leave it as it is for now as it'll be less confusing to make this kind of change in several places at once after your PR got merged.
src/util/allocate_objects.h
Outdated
| @@ -95,6 +95,10 @@ class allocate_objectst | |||
| const irep_idt &basename_prefix); | |||
| }; | |||
|
|
|||
| /// Create code allocating object of size `size` and assigning it to `lhs` | |||
| /// \param lhs : pointer which will be allocated | |||
| /// \param size : size of the object | |||
There was a problem hiding this comment.
Nit pick: no need for a space before colon
This utility function is only related to allocating an object and not to nondet-initialization. This also saves an include.
This allows us to call this function and assign the result to a code_assignt.
No functional change; the utility function can be used to directly replace the previous steps of creating the code_assignt.
Following the new coding standard.
This allows us to construct the expression in one line rather than three.
antlechner
force-pushed
the
antonia/move_make_allocate_code
branch
from
f80e3b1 to
b2e9778
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: b2e9778).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103670013
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.
No functional change, just some small refactoring.