Use goto_programt::make_X factories in goto_convert #4000
Conversation
kroening
commented
Jan 31, 2019
kroening
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.
- n/a 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).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
kroening
requested review from
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
| dest.add_instruction(SKIP); | ||
| dest.instructions.back().code.make_nil(); | ||
| dest.instructions.back().source_location=code.source_location(); | ||
| dest.add(goto_programt::make_skip(code.source_location())); |
There was a problem hiding this comment.
Looking at the use of these, couldn't we change the approach a bit and make goto_programt::add be a templated function taking a variadic number of arguments, with specialisations for the various instruction types?
template <goto_program_instruction_typet T, typename ... Params>
add(Params...);
template <> add<SKIP, source_locationt> (source_locationt loc) { ... };My rationale is that we might eventually forbid to construct an instructiont other than via .add, and it also saves us typing goto_programt::. The above would then be dest.add<SKIP>(code.source_location());
There was a problem hiding this comment.
Yes, I've been tempted by that idea. Will explore.
There was a problem hiding this comment.
It should be ok to merge all the make_X work as that does the hard work of collecting individual assignments into a single function call. Possibly moving to add<T>(...) is then just text transformation.
This avoids modification of instructiont::code after the object's creation.
This reduces code complexity.
| code_returnt c, | ||
| const source_locationt &l = source_locationt::nil()) | ||
| { | ||
| return instructiont(std::move(c), irep_idt(), l, RETURN, nil_exprt(), {}); |
There was a problem hiding this comment.
We need to make progress on #3126, which removes all these irep_idt() in the make_* functions.
| dest.add_instruction(SKIP); | ||
| dest.instructions.back().code.make_nil(); | ||
| dest.instructions.back().source_location=code.source_location(); | ||
| dest.add(goto_programt::make_skip(code.source_location())); |
There was a problem hiding this comment.
It should be ok to merge all the make_X work as that does the hard work of collecting individual assignments into a single function call. Possibly moving to add<T>(...) is then just text transformation.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 20a908d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99273103
