Replace use of #ifdef by template parameter in symex_assign #4840
Conversation
This would not compile when USE_UPDATE is activated.
This make it easier to detect problems in the code that does not get compiled, for instance here a missing ns argument, and open the possibility to unit-test both versions of the function.
Documentation was missing.
In shift_indexed_access_to_lhs. This makes sure both branches could compile correctly and open the possibility to test both branches.
In assign_array. This requires fixing some error in one of the branch since the compiler was not looking at it before.
In assign_struct_member. This requires fixing some problems in one of the branchs, as the compiler was not looking at it before.
romainbrenguier
requested review from
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 43fffdf).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/116945274
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
| } | ||
| else | ||
| return with_exprt{idx.array(), idx.index(), ssa_rhs}; | ||
| }(); |
There was a problem hiding this comment.
I don't get the point of this lambda function?!
There was a problem hiding this comment.
This is to make clear that this part of the code is just to find the new value of ssa_rhs. The alternative is to have directly an if statement and we wouldn't know what it's mutating without looking at the code inside the branches.
| new_rhs.where().set(ID_component_name, component_name); | ||
| return std::move(new_rhs); | ||
| } | ||
| }(); |
There was a problem hiding this comment.
Again, no idea why a lambda is the right thing here?
This make sure both branches could be compile (which was no longer the case), and open the possibility to unit-test both branches.