Clippy fixes

model-checking · Dec 19, 2023 · 39f7024 · 39f7024
1 parent 9b3b12e
commit 39f7024
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 8 deletions.
diff --git a/boogie_ast/src/boogie_program/mod.rs b/boogie_ast/src/boogie_program/mod.rs
@@ -188,7 +188,8 @@ impl Expr {
         Expr::FunctionCall { symbol, arguments }
     }
 
-    pub fn sign_extend(_e: Box<Expr>, _width: usize) -> Self {
+    pub fn sign_extend(e: Box<Expr>, _width: usize) -> Self {
+        let _e = e;
         todo!()
     }
 

diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use itertools::Itertools;
+use std::cmp::Ordering;
 use std::io::Write;
 
 use crate::kani_queries::QueryDb;
@@ -329,16 +330,14 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
                     let to = self.codegen_type(*ty);
                     let Type::Bv(from_width) = from else { panic!("Expecting bv type in cast") };
                     let Type::Bv(to_width) = to else { panic!("Expecting bv type in cast") };
-                    let op = if from_width > to_width {
-                        Expr::extract(Box::new(o), to_width, 0)
-                    } else if from_width < to_width {
-                        match from_type.kind() {
+                    let op = match from_width.cmp(&to_width) {
+                        Ordering::Greater => Expr::extract(Box::new(o), to_width, 0),
+                        Ordering::Less => match from_type.kind() {
                             ty::Int(_) => Expr::sign_extend(Box::new(o), to_width - from_width),
                             ty::Uint(_) => Expr::zero_extend(Box::new(o), to_width - from_width),
                             _ => todo!(),
-                        }
-                    } else {
-                        o
+                        },
+                        Ordering::Equal => o,
                     };
                     (None, op)
                 } else {