Skip to content

introduce exprt::visit_pre #4543

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.

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

Merged
merged 4 commits into from
Apr 17, 2019
Merged

introduce exprt::visit_pre #4543

merged 4 commits into from
Apr 17, 2019

Conversation

kroening
Copy link
Member

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

Daniel Kroening added 4 commits April 16, 2019 18:44
1) This offers a new interface for exprt::visit that uses a lambda.  The
suffix _pre clarifies that it does pre-order traversal.

2) The commit also introduces a template, which removes the redundancy
between the const and non-const variant.
This avoids stack overflows.
This avoids stack overflows.
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: 58736e3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108580350

@tautschnig tautschnig merged commit 4ef4cdc into develop Apr 17, 2019
@tautschnig tautschnig deleted the exprt_visit_pre branch April 17, 2019 07:53
@smowton
Copy link
Contributor

smowton commented Apr 17, 2019

Got to this one late, but I'd suggest any non-const visit is almost certainly a bad idea because it breaks all sharing -- use the depth iterator instead for that case. Const visit is good since there's no need to maintain the depth-iterator's stack if you're not going to make changes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants