Skip to content

use make_X API follow-up #4182

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 5 commits into from
Feb 26, 2019
Merged

use make_X API follow-up #4182

merged 5 commits into from
Feb 26, 2019

Conversation

kroening
Copy link
Member

@kroening kroening commented Feb 13, 2019 •
edited
Loading

This is follow up from #4177.

  • 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.

@kroening kroening changed the title Use make x5 use make_X API follow-up Feb 13, 2019
@kroening kroening force-pushed the use_make_X5 branch 2 times, most recently from 1c2bea5 to 2203dcd Compare February 14, 2019 08:50
tautschnig
tautschnig approved these changes Feb 14, 2019
View reviewed changes
@kroening kroening force-pushed the use_make_X5 branch 2 times, most recently from 610d836 to 2631fcb Compare February 14, 2019 09:00
@kroening kroening assigned thk123 and peterschrammel and unassigned kroening Feb 14, 2019
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.

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 2203dcd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100902365
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.

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.

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 610d836).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100907765
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.

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: 2631fcb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100910867

allredj
allredj reviewed Feb 16, 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: a5deeb0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101183449

allredj
allredj reviewed Feb 16, 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: 5520e05).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101188152

tautschnig
tautschnig requested changes Feb 26, 2019
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

(no action by anyone else needed, I'll take care of it) #4278 needs to be merged before this one to make sure the bug and bug fix are documented. I will then take care of rebasing this one on top of it.

Daniel Kroening added 5 commits February 26, 2019 12:25
@tautschnig
use instructiont::turn_into_skip
1f6762f 
This is a clearer idiom.
@tautschnig
prefer .add over .emplace
c6dba6a 
This is easier to read.
@tautschnig
use make_assignment(lhs, rhs)
9e596c9 
This is slightly shorter.
@tautschnig
avoid access to instructiont::code
82d7ce9 
This will allow protecting instructiont::code.
@tautschnig
use goto_programt::make_X
cba52e3 
This avoids incomplete construction.
@kroening kroening merged commit ca12c1c into develop Feb 26, 2019
@kroening kroening deleted the use_make_X5 branch February 26, 2019 13:57
allredj
allredj reviewed Feb 26, 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.

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: cba52e3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102331367
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.

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

@allredj allredj allredj left review comments

@thk123 thk123 thk123 approved these changes

@tautschnig tautschnig tautschnig approved these changes

@chrisr-diffblue chrisr-diffblue chrisr-diffblue approved these changes

@cesaro cesaro Awaiting requested review from cesaro

@cristina-david cristina-david Awaiting requested review from cristina-david

@danpoe danpoe Awaiting requested review from danpoe

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Awaiting requested review from hannes-steffenhagen-diffblue

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@NathanJPhillips NathanJPhillips Awaiting requested review from NathanJPhillips

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

@pkesseli pkesseli Awaiting requested review from pkesseli

@smowton smowton Awaiting requested review from smowton

@owen-mc-diffblue owen-mc-diffblue Awaiting requested review from owen-mc-diffblue

Assignees

@tautschnig tautschnig

Labels
cleanup
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@kroening @thk123 @tautschnig @allredj @chrisr-diffblue @peterschrammel