-
Notifications
You must be signed in to change notification settings - Fork 121
Closed
Labels
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.
Milestone
Description
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 account use ... as ...
statements.
We should instead correctly resolve names during stubbing, as well as support path constructs like self
and super
.
Metadata
Metadata
Assignees
Labels
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.