-
Notifications
You must be signed in to change notification settings - Fork 84
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 --legacy-linker
support
#2127
Remove --legacy-linker
support
#2127
Conversation
I updated the firecracker codegen test to use `cargo kani assess` instead and I removed the old scripts to collect info on the top X crates since we no longer use them. I kept the compiler option `--reachability=legacy` since we still use it to test the std library code generation. I also kept the `--mir-linker` option as a no-op for now.
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.
Happy to see this go. Thanks.
# Use the legacy linker for now since we want to maximize the code that we are compiling from firecracker. | ||
# The MIR Linker will by default only collect code relevant to proof harnesses, however, firecracker has none. | ||
cargo kani --only-codegen --legacy-linker | ||
# Use cargo assess since this is now our default way of assessing Kani suitability to verify a crate. |
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.
Not for this PR, but think we should do this for std
too? (Or did we already and I missed it...)
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.
We haven't. I added a note to the description of the PR.
I don't know how easy it would be to compile the tests of the std
library without the bootstrap script. We currently rely on the special cargo support to build the standard library. So even just building the standard library as part of cargo kani
flow would require a way to extend our cargo call to include the -Z build-std
.
Description of changes:
I updated the firecracker codegen test to use
cargo kani assess
instead and I removed the old scripts to collect info on the top X crates since we no longer use them.I kept the compiler option
--reachability=legacy
since we still use it to test the std library code generation. I also kept the--mir-linker
option as a no-op for now.Resolved issues:
Fixes #2126
Related RFC:
N/A
Call-outs:
Testing:
How is this change tested?
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.