Skip to content

Commit 554532c

Browse files
jsalzbergeduJacob Salzberg
and
Jacob Salzberg
authored
Fix "unused mut" warnings created by generated code. (rust-lang#3247)
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 ``` RESOLVES rust-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]>
1 parent 02ac268 commit 554532c

File tree

3 files changed

+9
-15
lines changed

3 files changed

+9
-15
lines changed

library/kani_macros/src/sysroot/contracts/bootstrap.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ impl<'a> ContractConditionsHandler<'a> {
8585

8686
let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
8787
self.output.extend(quote!(
88-
#[allow(dead_code, unused_variables)]
88+
#[allow(dead_code, unused_variables, unused_mut)]
8989
#[kanitool::is_contract_generated(recursion_wrapper)]
9090
#wrapper_sig {
9191
static mut REENTRY: bool = false;

library/kani_macros/src/sysroot/contracts/shared.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ impl<'a> ContractConditionsHandler<'a> {
5050
pub fn emit_common_header(&mut self) {
5151
if self.function_state.emit_tag_attr() {
5252
self.output.extend(quote!(
53-
#[allow(dead_code, unused_variables)]
53+
#[allow(dead_code, unused_variables, unused_mut)]
5454
));
5555
}
5656
self.output.extend(self.annotated_fn.attrs.iter().flat_map(Attribute::to_token_stream));

tests/expected/function-contract/gcd_success.rs

Lines changed: 7 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,28 +1,22 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
// kani-flags: -Zfunction-contracts
4+
#![deny(warnings)]
45
type T = u8;
56

67
/// Euclid's algorithm for calculating the GCD of two numbers
78
#[kani::requires(x != 0 && y != 0)]
89
#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)]
9-
fn gcd(x: T, y: T) -> T {
10-
let mut max = x;
11-
let mut min = y;
12-
if min > max {
13-
let val = max;
14-
max = min;
15-
min = val;
16-
}
17-
10+
fn gcd(mut x: T, mut y: T) -> T {
11+
(x, y) = (if x > y { x } else { y }, if x > y { y } else { x });
1812
loop {
19-
let res = max % min;
13+
let res = x % y;
2014
if res == 0 {
21-
return min;
15+
return y;
2216
}
2317

24-
max = min;
25-
min = res;
18+
x = y;
19+
y = res;
2620
}
2721
}
2822

0 commit comments

Comments
 (0)