-
Notifications
You must be signed in to change notification settings - Fork 277
Remove no-longer-used system_symbols #3605
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
Conversation
1f186b3
to
a086c36
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.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: a086c36).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95377889
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.
@peterschrammel @thk123 @allredj is this TG failure genuine? If so, is that cleanup or a proper bunch of work to be done on the TG side? |
Genuine failure - not immediately obvious to me how difficult it would be to resolve. It is using |
In this case you might just locally build a Urgency/scheduling all up to you, it's just noise disturbing my profiling :-) |
a086c36
to
ead71ee
Compare
This is a follow-up to the cleanup done in 2725a05. Creating a system_symbol_libraryt every time a languaget is created (effectively everytime from_expr is called) is costly, because of all the strings being looked up in the string table. On SV-COMP benchmarks, this accounted for 2% of runtime. Furthermore this removes this undesirable dependency on goto-programs from langapi.
ead71ee
to
749b4dd
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.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: ead71ee).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96759727
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.
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.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 749b4dd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96761629
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.
Just to say I've started looking at this now - will keep you updated. |
Bump made - will let you know when CI passes. |
Needed rebasing - #3916 |
Closing in favour #3916. |
This is a follow-up to the cleanup done in 2725a05. Creating a
system_symbol_libraryt every time a languaget is created (effectively everytime
from_expr is called) is costly, because of all the strings being looked up in
the string table. Furthermore this removes this undesirable dependency on
goto-prorgrams from langapi.