[Stubbing] Stubbing of trait method results in "unable to find `<...>` inside struct `<...>`"

[roypat]

I tried this code:

    trait Foo {
        fn foo() -> usize;
    }

    struct Bar;

    impl Foo for Bar {
        fn foo() -> usize {
            1
        }
    }

    fn foo_stub() -> usize {
        2
    }

    #[kani::proof]
    #[kani::stub(Bar::foo, foo_stub)]
    fn my_proof() {
        assert_eq!(Bar::foo(), 2)
    }

using the following command line invocation:

cargo kani  --enable-unstable --enable-stubbing --harness my_proof

with Kani version: 0.29.0

I expected to see this happen: Verification to pass, with the implementation of the foo trait method for Bar being stubbed out.

Instead, this happened:

error: failed to resolve `Bar::foo`: unable to find `foo` inside struct `Bar`
   --> <...>
    |
559 |     #[kani::stub(Bar::foo, foo_stub)]
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: this error originates in the attribute macro `kani::stub` (in Nightly builds, run with -Z macro-backtrace for more info)

[celinval]

Thanks for reporting this issue @roypat. I believe this is a duplicate of #1997. Let me know if the original issue covers your use case, and we can close this one. Thanks!

[celinval]

That said, I wonder if we should just split #1997 into two issues. We can use #1997 to track disambiguation using the qualified path type and use this issue to track stubbing trait methods without ambiguous definition. @feliperodri any thoughts?

[roypat]

Thanks for reporting this issue @roypat. I believe this is a duplicate of #1997. Let me know if the original issue covers your use case, and we can close this one. Thanks!

Ahhh, right, yes #1997 does indeed look like a general case of this. Sorry about that! Feel free to close as duplicate :)

[celinval]

BTW, @feliperodri I wonder if we can at least improve the error message now. We could add a note saying that trait methods are not supported.