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

Fix "unused mut" warnings created by generated code. #3247

Merged
merged 5 commits into from
Jun 10, 2024

Conversation

jsalzbergedu
Copy link
Contributor

@jsalzbergedu jsalzbergedu commented Jun 10, 2024

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 #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

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

RESOLVES #3010

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Because they duplicate, but don't neccessarily reuse, the parameters,
it is fine to mark them as "unused_mut".
@jsalzbergedu jsalzbergedu requested a review from a team as a code owner June 10, 2024 04:13
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Jun 10, 2024
@feliperodri feliperodri added this to the Function Contracts milestone Jun 10, 2024
@jsalzbergedu jsalzbergedu enabled auto-merge (squash) June 10, 2024 16:17
@jsalzbergedu jsalzbergedu merged commit 554532c into model-checking:main Jun 10, 2024
23 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

kani contracts cause false-positives for unused mut lint on the gcd example
2 participants