Repository navigation
Resolve names during stubbing #1866
Description
Activity
Would it be safe to assume that by correctly resolving names you would also be properly handling multiple versions of a crate? It might be nice to clarify that in the RFC.
Reacted by Aaron BembenekYes, we should be able to handle that.
Just to double check, in the case of multiple versions, one stub would only be applied to one specific version right?
That would be the optimal behavior, but it's going to take some experimenting with our path resolution algorithm to make sure we get this right. Luckily, it looks like clippy is in the process of updating its path resolution algorithm to handle this correctly (rust-lang/rust-clippy#9800), so we can probably draw from there.
It might actually be harder to handle multiple versions of the same crate than I thought, if they are included via the renaming-dependencies feature of Cargo. As far as I can tell, the data we have available at the MIR level refers to the original name of the crate, and not what it has been renamed to...
Closing this issue in favor of more specific ones.
Note that we have already implemented support for relative paths, including usage of
selfandsuper. I believe we are missing qualified paths needed for trait methods, and primitive type methods.
This issue affects how we treat the function/method names supplied in
kani::stub(<original>, <replacement>)attributes. We currently treat<original>and<replacement>verbatim as strings, so that they have to exactly match a name we find in the HIR. This means that we are unable to find many functions/methods in foreign crates, that we do not support relative paths, and that we are unable to take into accountuse ... as ...statements.We should instead correctly resolve names during stubbing, as well as support path constructs like
selfandsuper.