Fix "unused mut" warnings created by generated code.

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;

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));

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;
     }
 }