Skip to content

Don't use symex_dynamic:: magic string in multiple places #3481

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 1 commit into from
Feb 26, 2019
Merged

Don't use symex_dynamic:: magic string in multiple places #3481

merged 1 commit into from
Feb 26, 2019

Conversation

thk123
Copy link
Contributor

@thk123 thk123 commented Nov 30, 2018

  • 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.
  • 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).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

smowton
smowton reviewed Nov 30, 2018
View reviewed changes
src/util/simplify_expr_pointer.cpp Outdated
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
#include "simplify_expr_class.h"

#include <cassert>
#include <goto-symex/goto_symex.h>
Copy link
Contributor

Choose a reason for hiding this comment

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

I suspect that's a bad cross-module dependency (but then, so is utils knowing about symex internal magic)

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yeah looks like this particular simplification shouldn't be in util. Happy to either remove this particular usage - or pull the macro into util?

tautschnig
tautschnig requested changes Dec 1, 2018
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.

I'd suggest util/pointer_predicates.h as a place to store the macro and thus avoid the dependency problem noted by @smowton. There is a bigger story here with f1ff824 from #2646 doing essential cleanup.

@thk123 thk123 force-pushed the refactor/remove-symex-magic-string branch 2 times, most recently from 091e987 to f455438 Compare December 3, 2018 11:08
@thk123
Copy link
Contributor Author

thk123 commented Dec 3, 2018

@tautschnig @smowton dependency comment addressed

smowton
smowton approved these changes Dec 3, 2018
View reviewed changes
Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

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

Fine with this for now, but please make an issue to avoid non-symex modules having to know about a symex-specific magic identifier

@thk123 thk123 mentioned this pull request Dec 4, 2018
Open
@thk123
Copy link
Contributor Author

thk123 commented Dec 4, 2018

Done in #3526

allredj
allredj reviewed Dec 4, 2018
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: abe2102).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93531642
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.

@thk123
Copy link
Contributor Author

thk123 commented Dec 4, 2018

@tautschnig this is ready for a final review

tautschnig
tautschnig approved these changes Feb 25, 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.

My apologies for delaying this for such a long time. Looks good to me, but needs a rebase.

@tautschnig tautschnig assigned thk123 and unassigned tautschnig Feb 25, 2019
@thk123 thk123 force-pushed the refactor/remove-symex-magic-string branch from abe2102 to 10df3c0 Compare February 26, 2019 10:07
@thk123
Copy link
Contributor Author

thk123 commented Feb 26, 2019

Rebased and found another one.

@thk123 thk123 force-pushed the refactor/remove-symex-magic-string branch from 10df3c0 to 50df2a8 Compare February 26, 2019 10:08
@thk123 thk123 force-pushed the refactor/remove-symex-magic-string branch from 50df2a8 to 042ad74 Compare February 26, 2019 10:29
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.

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

@thk123
Copy link
Contributor Author

thk123 commented Feb 26, 2019

Time to play wack-a-mole with code owners - I need a goto-instrument code owner review:
@martin-cs @chrisr-diffblue @peterschrammel @danpoe @hannes-steffenhagen-diffblue

@tautschnig tautschnig merged commit 13b5e2b into diffblue:develop Feb 26, 2019
@thk123 thk123 deleted the refactor/remove-symex-magic-string branch February 26, 2019 14:27
@thk123 thk123 mentioned this pull request Feb 26, 2019
Merged
3 tasks
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

@smowton smowton smowton approved these changes

@tautschnig tautschnig tautschnig approved these changes

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

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

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

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

@pkesseli pkesseli Awaiting requested review from pkesseli

@danpoe danpoe Awaiting requested review from danpoe

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

Assignees

@danpoe danpoe

@chrisr-diffblue chrisr-diffblue

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
7 participants
@thk123 @smowton @tautschnig @allredj @chrisr-diffblue @danpoe @hannes-steffenhagen-diffblue