Move flatten_byte_* to lowering [blocks: #2068, #2501]#3290
Move flatten_byte_* to lowering [blocks: #2068, #2501]#3290kroening merged 2 commits intodiffblue:developfrom
Conversation
The operations in this code are not tied to Boolean flattening and instead do rewrites that are usable within any back-end.
The file will be substantially rewritten in follow-up commits and there is no need to do a large-scale whitespace change at this point.
allredj
left a comment
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 57f8848).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90582269
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.
| class namespacet; | ||
| class popcount_exprt; | ||
|
|
||
| exprt flatten_byte_extract(const byte_extract_exprt &src, const namespacet &ns); |
There was a problem hiding this comment.
If flattening is different from lowering then why are the functions in lowering called flattening?
There was a problem hiding this comment.
They will be renamed (I had already done so in 8cd566e), but I wanted to keep this one as easy as possible to review. I'll follow up with a PR doing the renaming shortly.
The operations in this code are not tied to Boolean flattening and instead do rewrites that are usable within any back-end.
This is a first step towards getting #2068 in a shape that can be reviewed and merged. No functional changes in this PR.