Enable Kani to verify the standard library crates #3152
Assignees
Comments
|
See rust-lang/wg-cargo-std-aware#7 for workarounds on how to build a modified |
celinval
added a commit
that referenced
this issue
Jun 10, 2024
…3245) Using stubs or function contracts as part of the `verify-std` sub-command does not work with multiple rustc executions as previous implementation. This happens because we now enable verifying dependencies, and cargo crashes due to a race condition. As soon as the first rustc invocation succeeds, cargo starts the compilation of the dependents crate. However, new executions can override files. Instead, we moved the stub logic to the new transformation framework, which is done on the top of the StableMIR body, and doesn't affect the Rust compiler session. We are now able to apply stub without restarting the compiler. This is a much better user experience as well, since multiple calls to the compiler can print the same warnings multiple times. Resolves #3072 Towards #3152 Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
|
We have added a sub-command to Kani ( |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
As we experiment with verifying the standard library, it might be helpful to enable users to verify the standard library crates directly, instead of having to create wrappers. Those wrappers can also only be used to verify public components.
There are a few things that need to be done in order to do that:
#[no_core]Kani library #3153Instrument contracts inI believe procedural macros are still allowed.corewithout proc_macros.kanimodule usingkani_corecrate.The text was updated successfully, but these errors were encountered: