You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I presume this is because the type is obtained by taking the type associated with the node-id of the free variable, which is a def_self that is probably generic to the impl, and not specialized to the method. The quick fix is to patch that code, perhaps the better fix is to have a distinct self-id per method? Not sure. It seems wrong to be baking in "if this is self, do something special" all over the place.
We do have a distinct self-id per method, as it turns out, but the type of it was tracked differently than regular variables, and as a result I missed updating it when explicit self went in. I'm fixing things to track the type of self in a more normal way.
This change adds "unused_mut" to the list of suppressed lints for
wrappers generated by the contracts macros. This will get rid of
spurious errors caused by mutable parameters to functions.
This fixes the example from
model-checking/kani#3010 .
It can be tested by adding the example from the issues to
tests/expected/test_macros/gcd.rs, creating a file
tests/expected/test_macros/gcd.expected, then running
```bash
cargo build-dev
RUST_BACKTRACE=1 cargo run -p compiletest -- --logfile logfile.txt --suite expected --mode expected --ignored --no-fail-fast --src-base tests/expected/test_macros
```
RESOLVESrust-lang#3010
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
---------
Co-authored-by: Jacob Salzberg <[email protected]>
Example test:
I presume this is because the type is obtained by taking the type associated with the node-id of the free variable, which is a def_self that is probably generic to the impl, and not specialized to the method. The quick fix is to patch that code, perhaps the better fix is to have a distinct self-id per method? Not sure. It seems wrong to be baking in "if this is self, do something special" all over the place.
@msullivan you may have an opinion.
The text was updated successfully, but these errors were encountered: