Skip to content

Resolve names during stubbing #1866

@aaronbembenek-aws

Description

@aaronbembenek-aws

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.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.

Type

No type

Projects

Relationships

None yet

Development

No branches or pull requests

Issue actions