-
Notifications
You must be signed in to change notification settings - Fork 134
Remove symbol table passes. #1932
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
This code hasn't been used since at least the creation of `kani-driver`. We might as well delete this.
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.
I'm in favor of removing this code because it complicates development when doing changes to our CProver API and it isn't used.
However, I don't see how this would resolve #444 . My understanding is that we're generating non-standard code for indexing SIMD vector components, as it's shown in --gen-c views, and the transformer just handles this case in a particular way.
Sorry, it wasn't clear to me from the issue description or comments. I'll post your comment there too. |
|
Actually, I read the #444 thread again and it actually makes sense. Sorry about it. |
No problem. Please wait for another review before merging. |
tedinski
left a comment
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.
I think I agree with this as well. Maybe @danielsn ?
|
Agreed. If we need this code, we can recreate it. Having unused code around adds toil without giving benifit. |
Description of changes:
This code hasn't been used since at least the creation of
kani-driver, and I don't think we have any plans to use it in the near future. We might as well delete this since it's likely broken by now (I think it was already broken beforekani-driver).Resolved issues:
Resolves #1384
This should also close the following opened issues related to
--gen-c-runnableCloses #445
Closes #441
Closes #439
Related RFC:
Call-outs:
Any objections to removing this code??? @danielsn
Testing:
How is this change tested? None. There was no test coverage for this.
Is this a refactor change?
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.