Skip to content
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

Improve stub resolution error #2013

Closed
celinval opened this issue Dec 16, 2022 · 1 comment · Fixed by #2227
Closed

Improve stub resolution error #2013

celinval opened this issue Dec 16, 2022 · 1 comment · Fixed by #2227
Assignees
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one.
Milestone

Comments

@celinval
Copy link
Contributor

Failure to resolve a stub source or target name is fairly generic. For the following stub:

#[kani::stub(orig2, self::other_crate2::mock)]

an error would look like:

error: unable to resolve function/method: crate::other_crate2::mock

We should be able to provide more information for the user. For example, was the problem found while trying to resolve other_crate2 or mock? Ideally we should also point out where the error is with span_error. Something like the resolution errors from the compiler:

error: cannot find `other_crate2` in the crate root
   --> src/lib.rs:10:20
   |
10 | #[kani::stub(orig2, self::other_crate2::mock)]
   |                           ^^^^^^^^^^^^ cannot find `other_crate2` in the crate root

@celinval celinval added [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. labels Dec 16, 2022
@celinval celinval added this to the Function/method stubbing milestone Dec 16, 2022
@celinval
Copy link
Contributor Author

I tried to improve the error message to provide more information on why the resolution failed. Unfortunately the span of the Ident that represent the path is the same span as the entire attribute.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one.
Projects
No open projects
Status: Done
Development

Successfully merging a pull request may close this issue.

1 participant