Skip to content

byte_extract lowering: ensure type consistency [blocks: #2068] #4063

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 2 commits into from
Feb 14, 2019
Merged

byte_extract lowering: ensure type consistency [blocks: #2068] #4063

merged 2 commits into from
Feb 14, 2019

Conversation

@tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Feb 3, 2019

Only the second commit is new, the first one is #4061.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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.

@tautschnig tautschnig self-assigned this Feb 4, 2019
@tautschnig tautschnig changed the title byte_extract lowering: ensure type consistency [depends-on: #4061, blocks: #2068] byte_extract lowering: ensure type consistency [depends-on: #4121, blocks: #2068] Feb 7, 2019
@tautschnig tautschnig self-assigned this Feb 7, 2019
@tautschnig tautschnig mentioned this pull request Feb 7, 2019
Merged
3 tasks
allredj
allredj reviewed Feb 7, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: dab949a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100131306

tautschnig added a commit that referenced this pull request Feb 14, 2019
@tautschnig
Merge pull request #4121 from tautschnig/smt-solver-cmake-tests
f4ed82a 
Cleanup of SMT2 solver test execution and CMake support [blocks: #4063]
@tautschnig
byte_extract lowering: ensure type consistency
a3d77e6 
Make sure we construct concatenations that are type consistent.
@tautschnig
The SMT back-end does not currently support bitvector -> union/struct…
8c154e2 
… conversion

Most of those shouldn't even be happening as more support needs to be
implemented in byte_extract_lowering. Will be taken care of in follow-up
commits.
@tautschnig tautschnig changed the title byte_extract lowering: ensure type consistency [depends-on: #4121, blocks: #2068] byte_extract lowering: ensure type consistency [blocks: #2068] Feb 14, 2019
@tautschnig tautschnig merged commit 02ce47f into diffblue:develop Feb 14, 2019
@tautschnig tautschnig deleted the byte-op-2 branch February 14, 2019 08:35
allredj
allredj reviewed Feb 14, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 8c154e2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100895849

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@forejtv forejtv Awaiting requested review from forejtv

@thk123 thk123 Awaiting requested review from thk123

2 more reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@tautschnig tautschnig

Labels

blocker bugfix

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@tautschnig @smowton @allredj @kroening @peterschrammel @chrisr-diffblue