From 554532cbef8732315d3c6b43c6c41eb64816b609 Mon Sep 17 00:00:00 2001
From: Jacob Salzberg <jsalzbergedu@yahoo.com>
Date: Mon, 10 Jun 2024 13:34:16 -0400
Subject: [PATCH] Fix "unused mut" warnings created by generated code. (#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
https://github.com/model-checking/kani/issues/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 #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 <salzber@amazon.com>
---
 .../src/sysroot/contracts/bootstrap.rs        |  2 +-
 .../src/sysroot/contracts/shared.rs           |  2 +-
 .../expected/function-contract/gcd_success.rs | 20 +++++++------------
 3 files changed, 9 insertions(+), 15 deletions(-)

diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
index 7c35cc469254..6a48bab08070 100644
--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
@@ -85,7 +85,7 @@ impl<'a> ContractConditionsHandler<'a> {
 
         let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
         self.output.extend(quote!(
-            #[allow(dead_code, unused_variables)]
+            #[allow(dead_code, unused_variables, unused_mut)]
             #[kanitool::is_contract_generated(recursion_wrapper)]
             #wrapper_sig {
                 static mut REENTRY: bool = false;
diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs
index b0f5804824ad..b0d323b12ca3 100644
--- a/library/kani_macros/src/sysroot/contracts/shared.rs
+++ b/library/kani_macros/src/sysroot/contracts/shared.rs
@@ -50,7 +50,7 @@ impl<'a> ContractConditionsHandler<'a> {
     pub fn emit_common_header(&mut self) {
         if self.function_state.emit_tag_attr() {
             self.output.extend(quote!(
-                #[allow(dead_code, unused_variables)]
+                #[allow(dead_code, unused_variables, unused_mut)]
             ));
         }
         self.output.extend(self.annotated_fn.attrs.iter().flat_map(Attribute::to_token_stream));
diff --git a/tests/expected/function-contract/gcd_success.rs b/tests/expected/function-contract/gcd_success.rs
index 3b983a230b60..61d8fea8ec80 100644
--- a/tests/expected/function-contract/gcd_success.rs
+++ b/tests/expected/function-contract/gcd_success.rs
@@ -1,28 +1,22 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
+#![deny(warnings)]
 type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
 #[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)]
-fn gcd(x: T, y: T) -> T {
-    let mut max = x;
-    let mut min = y;
-    if min > max {
-        let val = max;
-        max = min;
-        min = val;
-    }
-
+fn gcd(mut x: T, mut y: T) -> T {
+    (x, y) = (if x > y { x } else { y }, if x > y { y } else { x });
     loop {
-        let res = max % min;
+        let res = x % y;
         if res == 0 {
-            return min;
+            return y;
         }
 
-        max = min;
-        min = res;
+        x = y;
+        y = res;
     }
 }