-
Notifications
You must be signed in to change notification settings - Fork 274
Remove unnecessary uses of ns.follow in util/ #3737
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
Remove unnecessary uses of ns.follow in util/ #3737
Conversation
tautschnig
commented
Jan 9, 2019
- 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.
Am I wrong then in thinking a typedef manifests as a symbol type? |
typedef names are stored in |
BTW, the need to use type_eq() should go away -- simply equality should work. |
06b14ca
to
994ecbc
Compare
This also makes the namespace unnecessary in three cases.
Using ns.follow on both sides of an operator== is better encapsulated in type_eq.
Neither arrays nor Booleans use tag types.
There is no need to use ns.follow when either 1) we only compare the result to types that can never be hidden behind tags or 2) the tag case is handled explicitly.
994ecbc
to
d48e62b
Compare
There was a problem hiding this 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: d48e62b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98329813