diff --git a/cprover_bindings/src/cbmc_string.rs b/cprover_bindings/src/cbmc_string.rs
index 4c392f647759..d869b93a8570 100644
--- a/cprover_bindings/src/cbmc_string.rs
+++ b/cprover_bindings/src/cbmc_string.rs
@@ -3,9 +3,9 @@
 
 use lazy_static::lazy_static;
 use std::sync::Mutex;
+use string_interner::StringInterner;
 use string_interner::backend::StringBackend;
 use string_interner::symbol::SymbolU32;
-use string_interner::StringInterner;
 
 /// This class implements an interner for Strings.
 /// CBMC objects to have a large number of strings which refer to names: symbols, files, etc.
diff --git a/cprover_bindings/src/env.rs b/cprover_bindings/src/env.rs
index d31d213aa7d2..e4730c98d34c 100644
--- a/cprover_bindings/src/env.rs
+++ b/cprover_bindings/src/env.rs
@@ -8,8 +8,8 @@
 //! c.f. CBMC code [src/ansi-c/ansi_c_internal_additions.cpp].
 //! One possible invocation of this insertion in CBMC can be found in \[ansi_c_languaget::parse\].
 
-use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type};
 use super::MachineModel;
+use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type};
 use num::bigint::BigInt;
 fn int_constant<T>(name: &str, value: T) -> Symbol
 where
diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 16f33115e0ff..dad3b06e7753 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -285,13 +285,10 @@ pub fn arithmetic_overflow_result_type(operand_type: Type) -> Type {
     // give the struct the name "overflow_result_<type>", e.g.
     // "overflow_result_Unsignedbv"
     let name: InternedString = format!("overflow_result_{operand_type:?}").into();
-    Type::struct_type(
-        name,
-        vec![
-            DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
-            DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
-        ],
-    )
+    Type::struct_type(name, vec![
+        DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
+        DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
+    ])
 }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////
diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs
index 8b61722344fb..4d17be37f081 100644
--- a/cprover_bindings/src/goto_program/mod.rs
+++ b/cprover_bindings/src/goto_program/mod.rs
@@ -17,8 +17,8 @@ mod typ;
 
 pub use builtin::BuiltinFn;
 pub use expr::{
-    arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, Expr, ExprValue,
-    SelfOperator, UnaryOperator, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
+    ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, ArithmeticOverflowResult,
+    BinaryOperator, Expr, ExprValue, SelfOperator, UnaryOperator, arithmetic_overflow_result_type,
 };
 pub use location::Location;
 pub use stmt::{Stmt, StmtBody, SwitchCase};
diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs
index cd5bd8a6d967..97567670dee0 100644
--- a/cprover_bindings/src/goto_program/symbol_table.rs
+++ b/cprover_bindings/src/goto_program/symbol_table.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use super::super::{env, MachineModel};
+use super::super::{MachineModel, env};
 use super::{BuiltinFn, FunctionContract, Stmt, Symbol};
 use crate::InternedString;
 use std::collections::BTreeMap;
diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
index d0cc8821a447..3210dd46e43f 100644
--- a/cprover_bindings/src/goto_program/typ.rs
+++ b/cprover_bindings/src/goto_program/typ.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use self::DatatypeComponent::*;
 use self::Type::*;
-use super::super::utils::{aggr_tag, max_int, min_int};
 use super::super::MachineModel;
+use super::super::utils::{aggr_tag, max_int, min_int};
 use super::{Expr, SymbolTable};
 use crate::cbmc_string::InternedString;
 use std::collections::BTreeMap;
@@ -1598,10 +1598,10 @@ mod type_tests {
     fn check_typedef_struct_properties() {
         // Create a struct with a random field.
         let struct_name: InternedString = "MyStruct".into();
-        let struct_type = Type::struct_type(
-            struct_name,
-            vec![DatatypeComponent::Field { name: "field".into(), typ: Double }],
-        );
+        let struct_type = Type::struct_type(struct_name, vec![DatatypeComponent::Field {
+            name: "field".into(),
+            typ: Double,
+        }]);
         // Insert a field to the sym table to represent the struct field.
         let mut sym_table = SymbolTable::new(machine_model_test_stub());
         sym_table.ensure(struct_type.type_name().unwrap(), |_, name| {
diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs
index 6f821768f996..bb725de638cf 100644
--- a/cprover_bindings/src/irep/goto_binary_serde.rs
+++ b/cprover_bindings/src/irep/goto_binary_serde.rs
@@ -1205,12 +1205,12 @@ mod sharing_stats {
 mod tests {
     use super::GotoBinarySerializer;
     use super::IrepNumbering;
+    use crate::InternedString;
     use crate::cbmc_string::InternString;
-    use crate::irep::goto_binary_serde::GotoBinaryDeserializer;
     use crate::irep::Irep;
     use crate::irep::IrepId;
+    use crate::irep::goto_binary_serde::GotoBinaryDeserializer;
     use crate::linear_map;
-    use crate::InternedString;
     use linear_map::LinearMap;
     use std::io::BufWriter;
     /// Utility function : creates a Irep representing a single symbol.
diff --git a/cprover_bindings/src/irep/irep.rs b/cprover_bindings/src/irep/irep.rs
index 0d0c6dc4ace7..89da8e3446f5 100644
--- a/cprover_bindings/src/irep/irep.rs
+++ b/cprover_bindings/src/irep/irep.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! The actual `Irep` structure, and associated constructors, getters, and setters.
 
-use super::super::goto_program::{Location, Type};
 use super::super::MachineModel;
+use super::super::goto_program::{Location, Type};
 use super::{IrepId, ToIrep};
 use crate::cbmc_string::InternedString;
 use crate::linear_map;
diff --git a/cprover_bindings/src/irep/serialize.rs b/cprover_bindings/src/irep/serialize.rs
index bf3f0b807f61..06cc7bda17b9 100644
--- a/cprover_bindings/src/irep/serialize.rs
+++ b/cprover_bindings/src/irep/serialize.rs
@@ -1,10 +1,10 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! This crate implements irep serialization using serde Serializer.
-use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
 use crate::InternedString;
-use serde::ser::{SerializeMap, Serializer};
+use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
 use serde::Serialize;
+use serde::ser::{SerializeMap, Serializer};
 
 impl Serialize for Irep {
     fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
@@ -145,14 +145,16 @@ impl Serialize for Symbol {
 #[cfg(test)]
 mod test {
     use super::*;
-    use serde_test::{assert_ser_tokens, Token};
+    use serde_test::{Token, assert_ser_tokens};
     #[test]
     fn serialize_irep() {
         let irep = Irep::empty();
-        assert_ser_tokens(
-            &irep,
-            &[Token::Map { len: None }, Token::String("id"), Token::String("empty"), Token::MapEnd],
-        );
+        assert_ser_tokens(&irep, &[
+            Token::Map { len: None },
+            Token::String("id"),
+            Token::String("empty"),
+            Token::MapEnd,
+        ]);
     }
 
     #[test]
@@ -187,80 +189,77 @@ mod test {
             is_weak: false,
         };
         sym_table.insert(symbol);
-        assert_ser_tokens(
-            &sym_table,
-            &[
-                Token::Map { len: None },
-                Token::String("symbolTable"),
-                Token::Map { len: Some(1) },
-                Token::String("my_name"),
-                // symbol start
-                Token::Map { len: None },
-                // type irep
-                Token::String("type"),
-                Token::Map { len: None },
-                Token::String("id"),
-                Token::String("empty"),
-                Token::MapEnd,
-                // value irep
-                Token::String("value"),
-                Token::Map { len: None },
-                Token::String("id"),
-                Token::String("empty"),
-                Token::MapEnd,
-                // value locaton
-                Token::String("location"),
-                Token::Map { len: None },
-                Token::String("id"),
-                Token::String("empty"),
-                Token::MapEnd,
-                Token::String("name"),
-                Token::String("my_name"),
-                Token::String("module"),
-                Token::String(""),
-                Token::String("baseName"),
-                Token::String(""),
-                Token::String("prettyName"),
-                Token::String(""),
-                Token::String("mode"),
-                Token::String(""),
-                Token::String("isType"),
-                Token::Bool(false),
-                Token::String("isMacro"),
-                Token::Bool(false),
-                Token::String("isExported"),
-                Token::Bool(false),
-                Token::String("isInput"),
-                Token::Bool(false),
-                Token::String("isOutput"),
-                Token::Bool(false),
-                Token::String("isStateVar"),
-                Token::Bool(false),
-                Token::String("isProperty"),
-                Token::Bool(false),
-                Token::String("isStaticLifetime"),
-                Token::Bool(false),
-                Token::String("isThreadLocal"),
-                Token::Bool(false),
-                Token::String("isLvalue"),
-                Token::Bool(false),
-                Token::String("isFileLocal"),
-                Token::Bool(false),
-                Token::String("isExtern"),
-                Token::Bool(false),
-                Token::String("isVolatile"),
-                Token::Bool(false),
-                Token::String("isParameter"),
-                Token::Bool(false),
-                Token::String("isAuxiliary"),
-                Token::Bool(false),
-                Token::String("isWeak"),
-                Token::Bool(false),
-                Token::MapEnd,
-                Token::MapEnd,
-                Token::MapEnd,
-            ],
-        );
+        assert_ser_tokens(&sym_table, &[
+            Token::Map { len: None },
+            Token::String("symbolTable"),
+            Token::Map { len: Some(1) },
+            Token::String("my_name"),
+            // symbol start
+            Token::Map { len: None },
+            // type irep
+            Token::String("type"),
+            Token::Map { len: None },
+            Token::String("id"),
+            Token::String("empty"),
+            Token::MapEnd,
+            // value irep
+            Token::String("value"),
+            Token::Map { len: None },
+            Token::String("id"),
+            Token::String("empty"),
+            Token::MapEnd,
+            // value locaton
+            Token::String("location"),
+            Token::Map { len: None },
+            Token::String("id"),
+            Token::String("empty"),
+            Token::MapEnd,
+            Token::String("name"),
+            Token::String("my_name"),
+            Token::String("module"),
+            Token::String(""),
+            Token::String("baseName"),
+            Token::String(""),
+            Token::String("prettyName"),
+            Token::String(""),
+            Token::String("mode"),
+            Token::String(""),
+            Token::String("isType"),
+            Token::Bool(false),
+            Token::String("isMacro"),
+            Token::Bool(false),
+            Token::String("isExported"),
+            Token::Bool(false),
+            Token::String("isInput"),
+            Token::Bool(false),
+            Token::String("isOutput"),
+            Token::Bool(false),
+            Token::String("isStateVar"),
+            Token::Bool(false),
+            Token::String("isProperty"),
+            Token::Bool(false),
+            Token::String("isStaticLifetime"),
+            Token::Bool(false),
+            Token::String("isThreadLocal"),
+            Token::Bool(false),
+            Token::String("isLvalue"),
+            Token::Bool(false),
+            Token::String("isFileLocal"),
+            Token::Bool(false),
+            Token::String("isExtern"),
+            Token::Bool(false),
+            Token::String("isVolatile"),
+            Token::Bool(false),
+            Token::String("isParameter"),
+            Token::Bool(false),
+            Token::String("isAuxiliary"),
+            Token::Bool(false),
+            Token::String("isWeak"),
+            Token::Bool(false),
+            Token::MapEnd,
+            Token::MapEnd,
+            Token::MapEnd,
+        ]);
     }
 
     #[test]
@@ -269,41 +268,38 @@ mod test {
         let one_irep = Irep::one();
         let sub_irep = Irep::just_sub(vec![empty_irep.clone(), one_irep]);
         let top_irep = Irep::just_sub(vec![sub_irep, empty_irep]);
-        assert_ser_tokens(
-            &top_irep,
-            &[
-                // top_irep
-                Token::Map { len: None },
-                Token::String("id"),
-                Token::String(""),
-                Token::String("sub"),
-                Token::Seq { len: Some(2) },
-                // sub_irep
-                Token::Map { len: None },
-                Token::String("id"),
-                Token::String(""),
-                Token::String("sub"),
-                Token::Seq { len: Some(2) },
-                // empty_irep
-                Token::Map { len: None },
-                Token::String("id"),
-                Token::String("empty"),
-                Token::MapEnd,
-                // one_irep
-                Token::Map { len: None },
-                Token::String("id"),
-                Token::String("1"),
-                Token::MapEnd,
-                Token::SeqEnd,
-                Token::MapEnd,
-                // empty_irep
-                Token::Map { len: None },
-                Token::String("id"),
-                Token::String("empty"),
-                Token::MapEnd,
-                Token::SeqEnd,
-                Token::MapEnd,
-            ],
-        );
+        assert_ser_tokens(&top_irep, &[
+            // top_irep
+            Token::Map { len: None },
+            Token::String("id"),
+            Token::String(""),
+            Token::String("sub"),
+            Token::Seq { len: Some(2) },
+            // sub_irep
+            Token::Map { len: None },
+            Token::String("id"),
+            Token::String(""),
+            Token::String("sub"),
+            Token::Seq { len: Some(2) },
+            // empty_irep
+            Token::Map { len: None },
+            Token::String("id"),
+            Token::String("empty"),
+            Token::MapEnd,
+            // one_irep
+            Token::Map { len: None },
+            Token::String("id"),
+            Token::String("1"),
+            Token::MapEnd,
+            Token::SeqEnd,
+            Token::MapEnd,
+            // empty_irep
+            Token::Map { len: None },
+            Token::String("id"),
+            Token::String("empty"),
+            Token::MapEnd,
+            Token::SeqEnd,
+            Token::MapEnd,
+        ]);
     }
 }
diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs
index bf0b8ce862dd..788c9f1e79d4 100644
--- a/cprover_bindings/src/irep/to_irep.rs
+++ b/cprover_bindings/src/irep/to_irep.rs
@@ -2,11 +2,11 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! Converts a typed goto-program into the `Irep` serilization format of CBMC
 // TODO: consider making a macro to replace `linear_map![])` for initilizing btrees.
-use super::super::goto_program;
 use super::super::MachineModel;
+use super::super::goto_program;
 use super::{Irep, IrepId};
-use crate::linear_map;
 use crate::InternedString;
+use crate::linear_map;
 use goto_program::{
     BinaryOperator, CIntType, DatatypeComponent, Expr, ExprValue, Lambda, Location, Parameter,
     SelfOperator, Stmt, StmtBody, SwitchCase, SymbolValues, Type, UnaryOperator,
@@ -273,10 +273,12 @@ impl ToIrep for ExprValue {
                     )],
                 }
             }
-            ExprValue::FunctionCall { function, arguments } => side_effect_irep(
-                IrepId::FunctionCall,
-                vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
-            ),
+            ExprValue::FunctionCall { function, arguments } => {
+                side_effect_irep(IrepId::FunctionCall, vec![
+                    function.to_irep(mm),
+                    arguments_irep(arguments.iter(), mm),
+                ])
+            }
             ExprValue::If { c, t, e } => Irep {
                 id: IrepId::If,
                 sub: vec![c.to_irep(mm), t.to_irep(mm), e.to_irep(mm)],
@@ -318,10 +320,11 @@ impl ToIrep for ExprValue {
                 named_sub: linear_map![],
             },
             ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
-            ExprValue::StatementExpression { statements: ops, location: loc } => side_effect_irep(
-                IrepId::StatementExpression,
-                vec![Stmt::block(ops.to_vec(), *loc).to_irep(mm)],
-            ),
+            ExprValue::StatementExpression { statements: ops, location: loc } => {
+                side_effect_irep(IrepId::StatementExpression, vec![
+                    Stmt::block(ops.to_vec(), *loc).to_irep(mm),
+                ])
+            }
             ExprValue::StringConstant { s } => Irep {
                 id: IrepId::StringConstant,
                 sub: vec![],
@@ -488,10 +491,10 @@ impl ToIrep for StmtBody {
             StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]),
             StmtBody::Decl { lhs, value } => {
                 if value.is_some() {
-                    code_irep(
-                        IrepId::Decl,
-                        vec![lhs.to_irep(mm), value.as_ref().unwrap().to_irep(mm)],
-                    )
+                    code_irep(IrepId::Decl, vec![
+                        lhs.to_irep(mm),
+                        value.as_ref().unwrap().to_irep(mm),
+                    ])
                 } else {
                     code_irep(IrepId::Decl, vec![lhs.to_irep(mm)])
                 }
@@ -504,28 +507,26 @@ impl ToIrep for StmtBody {
                     .with_comment("deinit")
             }
             StmtBody::Expression(e) => code_irep(IrepId::Expression, vec![e.to_irep(mm)]),
-            StmtBody::For { init, cond, update, body } => code_irep(
-                IrepId::For,
-                vec![init.to_irep(mm), cond.to_irep(mm), update.to_irep(mm), body.to_irep(mm)],
-            ),
-            StmtBody::FunctionCall { lhs, function, arguments } => code_irep(
-                IrepId::FunctionCall,
-                vec![
+            StmtBody::For { init, cond, update, body } => code_irep(IrepId::For, vec![
+                init.to_irep(mm),
+                cond.to_irep(mm),
+                update.to_irep(mm),
+                body.to_irep(mm),
+            ]),
+            StmtBody::FunctionCall { lhs, function, arguments } => {
+                code_irep(IrepId::FunctionCall, vec![
                     lhs.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
                     function.to_irep(mm),
                     arguments_irep(arguments.iter(), mm),
-                ],
-            ),
+                ])
+            }
             StmtBody::Goto(dest) => code_irep(IrepId::Goto, vec![])
                 .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string())),
-            StmtBody::Ifthenelse { i, t, e } => code_irep(
-                IrepId::Ifthenelse,
-                vec![
-                    i.to_irep(mm),
-                    t.to_irep(mm),
-                    e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
-                ],
-            ),
+            StmtBody::Ifthenelse { i, t, e } => code_irep(IrepId::Ifthenelse, vec![
+                i.to_irep(mm),
+                t.to_irep(mm),
+                e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
+            ]),
             StmtBody::Label { label, body } => code_irep(IrepId::Label, vec![body.to_irep(mm)])
                 .with_named_sub(IrepId::Label, Irep::just_string_id(label.to_string())),
             StmtBody::Return(e) => {
@@ -537,10 +538,10 @@ impl ToIrep for StmtBody {
                 if default.is_some() {
                     switch_arms.push(switch_default_irep(default.as_ref().unwrap(), mm));
                 }
-                code_irep(
-                    IrepId::Switch,
-                    vec![control.to_irep(mm), code_irep(IrepId::Block, switch_arms)],
-                )
+                code_irep(IrepId::Switch, vec![
+                    control.to_irep(mm),
+                    code_irep(IrepId::Block, switch_arms),
+                ])
             }
             StmtBody::While { cond, body } => {
                 code_irep(IrepId::While, vec![cond.to_irep(mm), body.to_irep(mm)])
diff --git a/cprover_bindings/src/utils.rs b/cprover_bindings/src/utils.rs
index dd1d39ee53d1..4a323277ec9e 100644
--- a/cprover_bindings/src/utils.rs
+++ b/cprover_bindings/src/utils.rs
@@ -3,8 +3,8 @@
 //! Useful utilities for CBMC
 
 use crate::InternedString;
-use num::bigint::{BigInt, Sign};
 use num::Signed;
+use num::bigint::{BigInt, Sign};
 use num_traits::Zero;
 
 /// The aggregate name used in CBMC for aggregates of type `n`.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index c81d60e40d42..66d6e2eb1ab4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -19,8 +19,8 @@
 //!
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
+use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use rustc_middle::mir::coverage::SourceRegion;
 use stable_mir::mir::{Place, ProjectionElem};
 use stable_mir::ty::{Span as SpanStable, Ty};
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
index a871cd58f94f..26caf29bea1d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
@@ -1,16 +1,16 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::codegen_cprover_gotoc::{codegen::ty_stable::pointee_type_stable, GotocCtx};
+use crate::codegen_cprover_gotoc::{GotocCtx, codegen::ty_stable::pointee_type_stable};
 use crate::kani_middle::attributes::KaniAttributes;
 use cbmc::goto_program::FunctionContract;
 use cbmc::goto_program::{Expr, Lambda, Location, Type};
 use kani_metadata::AssignsContract;
 use rustc_hir::def_id::DefId as InternalDefId;
 use rustc_smir::rustc_internal;
+use stable_mir::CrateDef;
 use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::mir::{Local, VarDebugInfoContents};
 use stable_mir::ty::{FnDef, RigidTy, TyKind};
-use stable_mir::CrateDef;
 
 impl<'tcx> GotocCtx<'tcx> {
     /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
index 386a50bc7ebc..1a68533d3dce 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
@@ -9,17 +9,17 @@
 //! linking and usability unless unstable C-FFI support is enabled.
 use std::collections::HashSet;
 
-use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use cbmc::{InternString, InternedString};
 use lazy_static::lazy_static;
+use stable_mir::CrateDef;
 use stable_mir::abi::{CallConvention, PassMode};
-use stable_mir::mir::mono::Instance;
 use stable_mir::mir::Place;
+use stable_mir::mir::mono::Instance;
 use stable_mir::ty::{RigidTy, TyKind};
-use stable_mir::CrateDef;
 use tracing::{debug, trace};
 
 lazy_static! {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
index 34f8363f4948..eae547d58a4f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -3,14 +3,14 @@
 
 //! This file contains functions related to codegenning MIR functions into gotoc
 
-use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder;
 use crate::codegen_cprover_gotoc::GotocCtx;
-use cbmc::goto_program::{Expr, Stmt, Symbol};
+use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder;
 use cbmc::InternString;
+use cbmc::goto_program::{Expr, Stmt, Symbol};
+use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Body, Local};
 use stable_mir::ty::{RigidTy, TyKind};
-use stable_mir::CrateDef;
 use std::collections::BTreeMap;
 use tracing::{debug, debug_span};
 
@@ -223,8 +223,8 @@ pub mod rustc_smir {
     use rustc_middle::mir::coverage::MappingKind::Code;
     use rustc_middle::mir::coverage::SourceRegion;
     use rustc_middle::ty::TyCtxt;
-    use stable_mir::mir::mono::Instance;
     use stable_mir::Opaque;
+    use stable_mir::mir::mono::Instance;
 
     type CoverageOpaque = stable_mir::Opaque;
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 4b66d60e735b..79afe39fd89e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -2,16 +2,16 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! this module handles intrinsics
 use super::typ;
-use super::{bb_label, PropertyClass};
+use super::{PropertyClass, bb_label};
 use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
-use crate::codegen_cprover_gotoc::{utils, GotocCtx};
+use crate::codegen_cprover_gotoc::{GotocCtx, utils};
 use crate::intrinsics::Intrinsic;
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{
     ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type,
 };
-use rustc_middle::ty::layout::ValidityRequirement;
 use rustc_middle::ty::ParamEnv;
+use rustc_middle::ty::layout::ValidityRequirement;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{BasicBlockIdx, Operand, Place};
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 85bb8292ec67..3c67741667c2 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
 use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
 use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Symbol, Type};
 use rustc_middle::ty::Const as ConstInternal;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index d0e3fc3f442f..fb1ddb76e3a2 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -6,10 +6,10 @@
 //! in [GotocCtx::codegen_place] below.
 
 use super::typ::TypeExt;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type;
 use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
-use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type};
 use rustc_middle::ty::layout::LayoutOf;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 7abd949357ff..7a4594a181e3 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -1,21 +1,21 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace;
 use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
-use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::kani_middle::coercion::{
-    extract_unsize_casting_stable, CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBaseStable,
+    CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBaseStable, extract_unsize_casting_stable,
 };
 use crate::unwrap_or_return_codegen_unimplemented;
+use cbmc::MachineModel;
 use cbmc::goto_program::{
-    arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Type,
-    ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
+    ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, BinaryOperator, Expr, Location,
+    Stmt, Type, arithmetic_overflow_result_type,
 };
-use cbmc::MachineModel;
-use cbmc::{btree_string_map, InternString, InternedString};
+use cbmc::{InternString, InternedString, btree_string_map};
 use num::bigint::BigInt;
 use rustc_middle::ty::{ParamEnv, TyCtxt, VtblEntry};
 use rustc_smir::rustc_internal;
@@ -927,10 +927,10 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_discriminant_field(&self, place: Expr, ty: Ty) -> Expr {
         let layout = self.layout_of_stable(ty);
         assert!(
-            matches!(
-                &layout.variants,
-                Variants::Multiple { tag_encoding: TagEncoding::Direct, .. }
-            ),
+            matches!(&layout.variants, Variants::Multiple {
+                tag_encoding: TagEncoding::Direct,
+                ..
+            }),
             "discriminant field (`case`) only exists for multiple variants and direct encoding"
         );
         let expr = if ty.kind().is_coroutine() {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index ed0178511126..e54f962336d0 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -1,8 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use super::typ::TypeExt;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
-use super::{bb_label, PropertyClass};
+use super::typ::TypeExt;
+use super::{PropertyClass, bb_label};
 use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_coverage_opaque;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
@@ -15,7 +15,7 @@ use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
 use stable_mir::mir::mono::{Instance, InstanceKind};
 use stable_mir::mir::{
     AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place,
-    Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, RETURN_LOCAL,
+    RETURN_LOCAL, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
 };
 use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx};
 use tracing::{debug, debug_span, trace};
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
index 537fbcb63fbb..a45c3a8d69a0 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
@@ -5,8 +5,8 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::is_interior_mut;
-use stable_mir::mir::mono::{Instance, StaticDef};
 use stable_mir::CrateDef;
+use stable_mir::mir::mono::{Instance, StaticDef};
 use tracing::debug;
 
 impl<'tcx> GotocCtx<'tcx> {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 016bf0d3a261..ae45a2456794 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -6,10 +6,10 @@ use cbmc::utils::aggr_tag;
 use cbmc::{InternString, InternedString};
 use rustc_ast::ast::Mutability;
 use rustc_index::IndexVec;
+use rustc_middle::ty::GenericArgsRef;
 use rustc_middle::ty::layout::LayoutOf;
-use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::print::FmtPrinter;
-use rustc_middle::ty::GenericArgsRef;
+use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::{
     self, AdtDef, Const, CoroutineArgs, CoroutineArgsExt, FloatTy, Instance, IntTy, PolyFnSig, Ty,
     TyCtxt, TyKind, UintTy, VariantDef, VtblEntry,
@@ -22,8 +22,8 @@ use rustc_target::abi::{
     TyAndLayout, VariantIdx, Variants,
 };
 use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
-use stable_mir::mir::mono::Instance as InstanceStable;
 use stable_mir::mir::Body;
+use stable_mir::mir::mono::Instance as InstanceStable;
 use tracing::{debug, trace, warn};
 
 /// Map the unit type to an empty struct
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 9ef8bdf314c2..1efc41785351 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -6,7 +6,7 @@
 use crate::args::ReachabilityType;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::analysis;
-use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes};
+use crate::kani_middle::attributes::{KaniAttributes, is_test_harness_description};
 use crate::kani_middle::check_reachable_items;
 use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits};
 use crate::kani_middle::metadata::gen_test_metadata;
@@ -16,18 +16,18 @@ use crate::kani_middle::reachability::{
 };
 use crate::kani_middle::transform::{BodyTransformation, GlobalPasses};
 use crate::kani_queries::QueryDb;
+use cbmc::RoundingMode;
 use cbmc::goto_program::Location;
 use cbmc::irep::goto_binary_serde::write_goto_binary_file;
-use cbmc::RoundingMode;
 use cbmc::{InternedString, MachineModel};
-use kani_metadata::artifact::convert_type;
 use kani_metadata::UnsupportedFeature;
+use kani_metadata::artifact::convert_type;
 use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
 use kani_metadata::{AssignsContract, CompilerArtifactStub};
 use object::write::{self, StandardSegment, Symbol, SymbolSection};
 use object::{
-    elf, pe, xcoff, Architecture, BinaryFormat, Endianness, FileFlags, SectionFlags, SectionKind,
-    SubArchitecture, SymbolFlags, SymbolKind, SymbolScope,
+    Architecture, BinaryFormat, Endianness, FileFlags, SectionFlags, SectionKind, SubArchitecture,
+    SymbolFlags, SymbolKind, SymbolScope, elf, pe, xcoff,
 };
 use rustc_codegen_ssa::back::archive::{ArArchiveBuilder, ArchiveBuilder, DEFAULT_OBJECT_READER};
 use rustc_codegen_ssa::back::metadata::create_metadata_file_for_wasm;
@@ -35,20 +35,20 @@ use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_codegen_ssa::{CodegenResults, CrateInfo};
 use rustc_data_structures::fx::{FxHashMap, FxIndexMap};
 use rustc_data_structures::temp_dir::MaybeTempDir;
-use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
+use rustc_errors::{DEFAULT_LOCALE_RESOURCE, ErrorGuaranteed};
 use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE};
-use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
+use rustc_metadata::fs::{METADATA_FILENAME, emit_wrapper_file};
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::util::Providers;
+use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
-use rustc_session::Session;
 use rustc_smir::rustc_internal;
 use rustc_span::sym;
 use rustc_target::abi::Endian;
-use rustc_target::spec::{ef_avr_arch, PanicStrategy, RelocModel, Target};
+use rustc_target::spec::{PanicStrategy, RelocModel, Target, ef_avr_arch};
 use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::{CrateDef, DefId};
 use std::any::Any;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
index ea3c9e909eb6..246b6cd94b47 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
@@ -2,13 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use cbmc::goto_program::Stmt;
 use cbmc::InternedString;
+use cbmc::goto_program::Stmt;
 use rustc_middle::ty::Instance as InstanceInternal;
 use rustc_smir::rustc_internal;
-use stable_mir::mir::mono::Instance;
-use stable_mir::mir::{visit::Location, visit::MirVisitor, Body, Local, LocalDecl, Rvalue};
 use stable_mir::CrateDef;
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::{Body, Local, LocalDecl, Rvalue, visit::Location, visit::MirVisitor};
 use std::collections::{HashMap, HashSet};
 
 /// This structure represents useful data about the function we are currently compiling.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 3f17f4b87233..d88506464cf7 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -16,9 +16,9 @@
 //! this structure as input.
 use super::current_fn::CurrentFnCtx;
 use super::vtable_ctx::VtableCtx;
-use crate::codegen_cprover_gotoc::overrides::{fn_hooks, GotocHooks};
-use crate::codegen_cprover_gotoc::utils::full_crate_name;
 use crate::codegen_cprover_gotoc::UnsupportedConstructs;
+use crate::codegen_cprover_gotoc::overrides::{GotocHooks, fn_hooks};
+use crate::codegen_cprover_gotoc::utils::full_crate_name;
 use crate::kani_middle::transform::BodyTransformation;
 use crate::kani_queries::QueryDb;
 use cbmc::goto_program::{
@@ -33,12 +33,12 @@ use rustc_middle::ty::layout::{
     TyAndLayout,
 };
 use rustc_middle::ty::{self, Ty, TyCtxt};
-use rustc_span::source_map::respan;
 use rustc_span::Span;
+use rustc_span::source_map::respan;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
-use stable_mir::mir::mono::Instance;
 use stable_mir::mir::Body;
+use stable_mir::mir::mono::Instance;
 use stable_mir::ty::Allocation;
 use std::fmt::Debug;
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs
index 98e78ed2b5fd..854ddf6baa57 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs
@@ -1,6 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+use crate::codegen_cprover_gotoc::GotocCtx;
 /// We can improve verification performance by conveying semantic information
 /// about function pointer calls down to the underlying solver. In particular,
 /// method calls through Rust dynamic trait objects use a vtable (virtual method
@@ -16,9 +17,8 @@
 /// For the current CBMC implementation of function restrictions, see:
 ///     http://cprover.diffblue.com/md__home_travis_build_diffblue_cbmc_doc_architectural_restrict-function-pointer.html
 use crate::codegen_cprover_gotoc::codegen::typ::pointee_type;
-use crate::codegen_cprover_gotoc::GotocCtx;
-use cbmc::goto_program::{Stmt, Type};
 use cbmc::InternedString;
+use cbmc::goto_program::{Stmt, Type};
 use kani_metadata::{CallSite, PossibleMethodEntry, TraitDefinedMethod, VtableCtxResults};
 use rustc_data_structures::fx::FxHashMap;
 use tracing::debug;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index c0df279932f6..da3cef9e3564 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -8,8 +8,8 @@
 //! It would be too nasty if we spread around these sort of undocumented hooks in place, so
 //! this module addresses this issue.
 
-use crate::codegen_cprover_gotoc::codegen::{bb_label, PropertyClass};
 use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::codegen_cprover_gotoc::codegen::{PropertyClass, bb_label};
 use crate::kani_middle::attributes::matches_diagnostic as matches_function;
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{BuiltinFn, Expr, Stmt, Type};
@@ -17,7 +17,7 @@ use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{BasicBlockIdx, Place};
-use stable_mir::{ty::Span, CrateDef};
+use stable_mir::{CrateDef, ty::Span};
 use std::rc::Rc;
 use tracing::debug;
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/mod.rs
index 3dda5076fb89..1ba563527626 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/mod.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/mod.rs
@@ -8,4 +8,4 @@
 
 mod hooks;
 
-pub use hooks::{fn_hooks, GotocHooks};
+pub use hooks::{GotocHooks, fn_hooks};
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
index 0c69cb30b37f..fe19c854c2ac 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
@@ -5,9 +5,9 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
-use stable_mir::mir::mono::Instance;
-use stable_mir::mir::Body;
 use stable_mir::CrateDef;
+use stable_mir::mir::Body;
+use stable_mir::mir::mono::Instance;
 use std::cell::RefCell;
 use std::panic;
 use std::sync::LazyLock;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
index 16edca2a826c..faf1ed61dc2f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
@@ -3,7 +3,7 @@
 use super::super::codegen::TypeExt;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, ExprValue, Location, SymbolTable, Type};
-use cbmc::{btree_string_map, InternedString};
+use cbmc::{InternedString, btree_string_map};
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use stable_mir::ty::Span;
diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs
index 9485d8525410..13a12751bd07 100644
--- a/kani-compiler/src/intrinsics.rs
+++ b/kani-compiler/src/intrinsics.rs
@@ -4,7 +4,7 @@
 //! Single source of truth about which intrinsics we support.
 
 use stable_mir::{
-    mir::{mono::Instance, Mutability},
+    mir::{Mutability, mono::Instance},
     ty::{FloatTy, IntTy, RigidTy, TyKind, UintTy},
 };
 
diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs
index 0adee0e52cca..b232db8feecb 100644
--- a/kani-compiler/src/kani_middle/analysis.rs
+++ b/kani-compiler/src/kani_middle/analysis.rs
@@ -9,7 +9,7 @@
 
 use stable_mir::mir::mono::MonoItem;
 use stable_mir::mir::{
-    visit::Location, MirVisitor, Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
+    MirVisitor, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, visit::Location,
 };
 use std::collections::HashMap;
 use std::fmt::Display;
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 86e97f633dfb..630f818231c9 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -7,7 +7,7 @@ use std::collections::BTreeMap;
 use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
 use quote::ToTokens;
 use rustc_ast::{
-    attr, AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind,
+    AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, attr,
 };
 use rustc_errors::ErrorGuaranteed;
 use rustc_hir::{def::DefKind, def_id::DefId};
@@ -25,7 +25,7 @@ use syn::{PathSegment, TypePath};
 
 use tracing::{debug, trace};
 
-use super::resolve::{resolve_fn, resolve_fn_path, FnResolution, ResolveError};
+use super::resolve::{FnResolution, ResolveError, resolve_fn, resolve_fn_path};
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)]
 #[strum(serialize_all = "snake_case")]
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index d16e4d2b93d1..071e880ffd9f 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -19,9 +19,9 @@ use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::OutputType;
 use rustc_smir::rustc_internal;
+use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
 use stable_mir::ty::{FnDef, IndexedVal, RigidTy, TyKind};
-use stable_mir::CrateDef;
 use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
 use std::fs::File;
 use std::io::BufWriter;
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 38760fca300d..224abef1b02b 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -15,12 +15,12 @@
 
 use rustc_hir::lang_items::LangItem;
 use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
-use rustc_middle::ty::adjustment::CustomCoerceUnsized;
 use rustc_middle::ty::TraitRef;
+use rustc_middle::ty::adjustment::CustomCoerceUnsized;
 use rustc_middle::ty::{ParamEnv, Ty, TyCtxt};
 use rustc_smir::rustc_internal;
-use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
 use stable_mir::Symbol;
+use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
 use tracing::trace;
 
 /// Given an unsized coercion (e.g. from `&u8` to `&dyn Debug`), extract the pair of
diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs
index 73e42be00e7b..c32ec38a3696 100644
--- a/kani-compiler/src/kani_middle/intrinsics.rs
+++ b/kani-compiler/src/kani_middle/intrinsics.rs
@@ -8,7 +8,7 @@ use rustc_middle::mir::{Local, LocalDecl};
 use rustc_middle::ty::{self, Ty, TyCtxt};
 use rustc_middle::ty::{Const, GenericArgsRef, IntrinsicDef};
 use rustc_span::source_map::Spanned;
-use rustc_span::symbol::{sym, Symbol};
+use rustc_span::symbol::{Symbol, sym};
 use tracing::{debug, trace};
 
 pub struct ModelIntrinsics<'tcx> {
diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs
index 2f0f22d49e1c..db6b6b06149a 100644
--- a/kani-compiler/src/kani_middle/metadata.rs
+++ b/kani-compiler/src/kani_middle/metadata.rs
@@ -8,10 +8,10 @@ use std::path::Path;
 use crate::kani_middle::attributes::test_harness_name;
 use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata};
 use rustc_middle::ty::TyCtxt;
-use stable_mir::mir::mono::Instance;
 use stable_mir::CrateDef;
+use stable_mir::mir::mono::Instance;
 
-use super::{attributes::KaniAttributes, SourceLocation};
+use super::{SourceLocation, attributes::KaniAttributes};
 
 /// Create the harness metadata for a proof harness for a given function.
 pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata {
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index f281e5de5e88..5f7f4c28068f 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -14,14 +14,14 @@ use rustc_middle::ty::layout::{
 };
 use rustc_middle::ty::{self, Instance as InstanceInternal, Ty as TyInternal, TyCtxt};
 use rustc_smir::rustc_internal;
-use rustc_span::source_map::respan;
 use rustc_span::Span;
+use rustc_span::source_map::respan;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
+use stable_mir::CrateDef;
 use stable_mir::mir::mono::MonoItem;
 use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind};
 use stable_mir::visitor::{Visitable, Visitor as TyVisitor};
-use stable_mir::CrateDef;
 use std::ops::ControlFlow;
 
 use self::attributes::KaniAttributes;
diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
index 68343ccaad37..040a925e140f 100644
--- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
+++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
@@ -42,8 +42,8 @@ use rustc_middle::{
 };
 use rustc_mir_dataflow::{Analysis, AnalysisDomain, Forward, JoinSemiLattice};
 use rustc_smir::rustc_internal;
-use rustc_span::{source_map::Spanned, DUMMY_SP};
-use stable_mir::mir::{mono::Instance as StableInstance, Body as StableBody};
+use rustc_span::{DUMMY_SP, source_map::Spanned};
+use stable_mir::mir::{Body as StableBody, mono::Instance as StableInstance};
 use std::collections::HashSet;
 
 /// Main points-to analysis object.
@@ -458,22 +458,19 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
             // Sanity check. The first argument is the closure itself and the second argument is the tupled arguments from the caller.
             assert!(args.len() == 2);
             // First, connect all upvars.
-            let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(
-                instance,
-                Place { local: 1usize.into(), projection: List::empty() },
-            )]);
+            let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place {
+                local: 1usize.into(),
+                projection: List::empty(),
+            })]);
             let rvalue_set = self.successors_for_operand(state, args[0].node.clone());
             initial_graph.extend(&lvalue_set, &rvalue_set);
             // Then, connect the argument tuple to each of the spread arguments.
             let spread_arg_operand = args[1].node.clone();
             for i in 0..new_body.arg_count {
-                let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(
-                    instance,
-                    Place {
-                        local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that.
-                        projection: List::empty(),
-                    },
-                )]);
+                let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place {
+                    local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that.
+                    projection: List::empty(),
+                })]);
                 // This conservatively assumes all arguments alias to all parameters.
                 let rvalue_set = self.successors_for_operand(state, spread_arg_operand.clone());
                 initial_graph.extend(&lvalue_set, &rvalue_set);
@@ -481,13 +478,10 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
         } else {
             // Otherwise, simply connect all arguments to parameters.
             for (i, arg) in args.iter().enumerate() {
-                let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(
-                    instance,
-                    Place {
-                        local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that.
-                        projection: List::empty(),
-                    },
-                )]);
+                let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place {
+                    local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that.
+                    projection: List::empty(),
+                })]);
                 let rvalue_set = self.successors_for_operand(state, arg.node.clone());
                 initial_graph.extend(&lvalue_set, &rvalue_set);
             }
@@ -501,10 +495,10 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
 
         // Connect the return value to the return destination.
         let lvalue_set = state.resolve_place(*destination, self.instance);
-        let rvalue_set = HashSet::from([MemLoc::new_stack_allocation(
-            instance,
-            Place { local: 0usize.into(), projection: List::empty() },
-        )]);
+        let rvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place {
+            local: 0usize.into(),
+            projection: List::empty(),
+        })]);
         state.extend(&lvalue_set, &state.successors(&rvalue_set));
     }
 
diff --git a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs
index 61804d0ff71a..4dd2fba62fb0 100644
--- a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs
+++ b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs
@@ -8,11 +8,11 @@ use rustc_middle::{
     mir::{Location, Place, ProjectionElem},
     ty::{Instance, List, TyCtxt},
 };
-use rustc_mir_dataflow::{fmt::DebugWithContext, JoinSemiLattice};
+use rustc_mir_dataflow::{JoinSemiLattice, fmt::DebugWithContext};
 use rustc_smir::rustc_internal;
 use stable_mir::mir::{
-    mono::{Instance as StableInstance, StaticDef},
     Place as StablePlace,
+    mono::{Instance as StableInstance, StaticDef},
 };
 use std::collections::{HashMap, HashSet, VecDeque};
 
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index b808a5c5b8ee..6f2e779320f3 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -24,14 +24,14 @@ use rustc_data_structures::stable_hasher::{HashStable, StableHasher};
 use rustc_middle::ty::{TyCtxt, VtblEntry};
 use rustc_session::config::OutputType;
 use rustc_smir::rustc_internal;
+use stable_mir::CrateItem;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef};
 use stable_mir::mir::{
-    visit::Location, Body, CastKind, ConstOperand, MirVisitor, PointerCoercion, Rvalue, Terminator,
-    TerminatorKind,
+    Body, CastKind, ConstOperand, MirVisitor, PointerCoercion, Rvalue, Terminator, TerminatorKind,
+    visit::Location,
 };
 use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind};
-use stable_mir::CrateItem;
 use stable_mir::{CrateDef, ItemKind};
 use std::fmt::{Display, Formatter};
 use std::{
diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index d2b1fcd06471..d71f9710d404 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -14,13 +14,13 @@ use crate::kani_middle::stable_fn_def;
 use quote::ToTokens;
 use rustc_errors::ErrorGuaranteed;
 use rustc_hir::def::{DefKind, Res};
-use rustc_hir::def_id::{DefId, LocalDefId, LocalModDefId, CRATE_DEF_INDEX, LOCAL_CRATE};
+use rustc_hir::def_id::{CRATE_DEF_INDEX, DefId, LOCAL_CRATE, LocalDefId, LocalModDefId};
 use rustc_hir::{ItemKind, UseKind};
-use rustc_middle::ty::fast_reject::{self, TreatParams};
 use rustc_middle::ty::TyCtxt;
+use rustc_middle::ty::fast_reject::{self, TreatParams};
 use rustc_smir::rustc_internal;
-use stable_mir::ty::{FnDef, RigidTy, Ty, TyKind};
 use stable_mir::CrateDef;
+use stable_mir::ty::{FnDef, RigidTy, Ty, TyKind};
 use std::collections::HashSet;
 use std::fmt;
 use std::iter::Peekable;
diff --git a/kani-compiler/src/kani_middle/resolve/type_resolution.rs b/kani-compiler/src/kani_middle/resolve/type_resolution.rs
index 790019ab2998..9e594785a122 100644
--- a/kani-compiler/src/kani_middle/resolve/type_resolution.rs
+++ b/kani-compiler/src/kani_middle/resolve/type_resolution.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! This module contains code used for resolve type / trait names
 
-use crate::kani_middle::resolve::{resolve_path, validate_kind, ResolveError};
+use crate::kani_middle::resolve::{ResolveError, resolve_path, validate_kind};
 use quote::ToTokens;
 use rustc_hir::def::DefKind;
 use rustc_middle::ty::TyCtxt;
diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs
index f145a4d105e2..4a48c649983c 100644
--- a/kani-compiler/src/kani_middle/stubbing/mod.rs
+++ b/kani-compiler/src/kani_middle/stubbing/mod.rs
@@ -14,9 +14,9 @@ use rustc_hir::def_id::DefId;
 use rustc_middle::mir::Const;
 use rustc_middle::ty::{self, EarlyBinder, ParamEnv, TyCtxt, TypeFoldable};
 use rustc_smir::rustc_internal;
+use stable_mir::mir::ConstOperand;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::visit::{Location, MirVisitor};
-use stable_mir::mir::ConstOperand;
 use stable_mir::ty::{FnDef, RigidTy, TyKind};
 use stable_mir::{CrateDef, CrateItem};
 
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs
index 35d0e7041704..dfd16594146f 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs
@@ -10,11 +10,11 @@ use crate::{
 };
 use stable_mir::{
     mir::{
+        Body, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, Rvalue,
+        Statement, StatementKind, Terminator, TerminatorKind,
         alloc::GlobalAlloc,
         mono::{Instance, InstanceKind, StaticDef},
         visit::Location,
-        Body, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, Rvalue,
-        Statement, StatementKind, Terminator, TerminatorKind,
     },
     ty::{ConstantKind, RigidTy, TyKind},
 };
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
index 41a2b69d1fdf..877ff41ea6d5 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
@@ -9,16 +9,16 @@ use crate::kani_middle::{
     transform::{
         body::{InsertPosition, MutableBody, SourceInstruction},
         check_uninit::{
-            relevant_instruction::{InitRelevantInstruction, MemoryInitOp},
             TargetFinder,
+            relevant_instruction::{InitRelevantInstruction, MemoryInitOp},
         },
     },
 };
 use rustc_middle::ty::TyCtxt;
 use stable_mir::mir::{
+    MirVisitor, Operand, Place, Rvalue, Statement, Terminator,
     mono::Instance,
     visit::{Location, PlaceContext},
-    MirVisitor, Operand, Place, Rvalue, Statement, Terminator,
 };
 use std::collections::HashSet;
 
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs
index c31f72c9b5c3..b2a7ffd13bc1 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs
@@ -8,11 +8,11 @@ use std::collections::HashSet;
 
 use crate::args::ExtraChecks;
 use crate::kani_middle::{
-    points_to::{run_points_to_analysis, MemLoc, PointsToGraph},
+    points_to::{MemLoc, PointsToGraph, run_points_to_analysis},
     reachability::CallGraph,
     transform::{
-        body::CheckType, check_uninit::UninitInstrumenter, BodyTransformation, GlobalPass,
-        TransformationResult,
+        BodyTransformation, GlobalPass, TransformationResult, body::CheckType,
+        check_uninit::UninitInstrumenter,
     },
 };
 use crate::kani_queries::QueryDb;
@@ -22,8 +22,8 @@ use rustc_middle::ty::TyCtxt;
 use rustc_mir_dataflow::JoinSemiLattice;
 use rustc_session::config::OutputType;
 use stable_mir::{
-    mir::mono::{Instance, MonoItem},
     mir::MirVisitor,
+    mir::mono::{Instance, MonoItem},
     ty::FnDef,
 };
 
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
index 726dc1965770..1ce21ef50669 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
@@ -12,12 +12,12 @@ use relevant_instruction::{InitRelevantInstruction, MemoryInitOp};
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use stable_mir::{
+    CrateDef,
     mir::{
-        mono::Instance, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, Operand, Place,
-        Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction,
+        AggregateKind, BasicBlock, Body, ConstOperand, Mutability, Operand, Place, Rvalue,
+        Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, mono::Instance,
     },
     ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy},
-    CrateDef,
 };
 use std::collections::HashMap;
 
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs
index 37f1d94ed744..2408a3b50a6c 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs
@@ -6,17 +6,17 @@
 
 use crate::args::ExtraChecks;
 use crate::kani_middle::transform::{
-    body::{CheckType, InsertPosition, MutableBody, SourceInstruction},
-    check_uninit::{get_mem_init_fn_def, UninitInstrumenter},
     TransformPass, TransformationType,
+    body::{CheckType, InsertPosition, MutableBody, SourceInstruction},
+    check_uninit::{UninitInstrumenter, get_mem_init_fn_def},
 };
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use stable_mir::{
-    mir::{mono::Instance, Body, Mutability, Place},
-    ty::{FnDef, GenericArgs, Ty},
     CrateDef,
+    mir::{Body, Mutability, Place, mono::Instance},
+    ty::{FnDef, GenericArgs, Ty},
 };
 use std::collections::HashMap;
 use std::fmt::Debug;
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs
index bd4356017b6b..20f4538453b5 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs
@@ -8,20 +8,20 @@ use crate::{
     kani_middle::transform::{
         body::{InsertPosition, MutableBody, SourceInstruction},
         check_uninit::{
-            relevant_instruction::{InitRelevantInstruction, MemoryInitOp},
-            ty_layout::{tys_layout_compatible_to_size, LayoutComputationError},
             PointeeInfo, TargetFinder,
+            relevant_instruction::{InitRelevantInstruction, MemoryInitOp},
+            ty_layout::{LayoutComputationError, tys_layout_compatible_to_size},
         },
     },
 };
 use stable_mir::{
     mir::{
-        alloc::GlobalAlloc,
-        mono::{Instance, InstanceKind},
-        visit::{Location, PlaceContext},
         AggregateKind, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place,
         PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator,
         TerminatorKind,
+        alloc::GlobalAlloc,
+        mono::{Instance, InstanceKind},
+        visit::{Location, PlaceContext},
     },
     ty::{AdtKind, ConstantKind, RigidTy, TyKind},
 };
diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
index a81f76d25393..d0fd553ef5cf 100644
--- a/kani-compiler/src/kani_middle/transform/check_values.rs
+++ b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -22,6 +22,7 @@ use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::{Const, TyCtxt};
 use rustc_smir::rustc_internal;
+use stable_mir::CrateDef;
 use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, WrappingRange};
 use stable_mir::mir::mono::{Instance, InstanceKind};
 use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef};
@@ -32,7 +33,6 @@ use stable_mir::mir::{
 };
 use stable_mir::target::{MachineInfo, MachineSize};
 use stable_mir::ty::{AdtKind, IndexedVal, MirConst, RigidTy, Ty, TyKind, UintTy};
-use stable_mir::CrateDef;
 use std::fmt::Debug;
 use strum_macros::AsRefStr;
 use tracing::{debug, trace};
diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs
index 71e06f5c49cd..480c480a0aea 100644
--- a/kani-compiler/src/kani_middle/transform/contracts.rs
+++ b/kani-compiler/src/kani_middle/transform/contracts.rs
@@ -12,12 +12,12 @@ use rustc_hir::def_id::DefId as InternalDefId;
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use rustc_span::Symbol;
+use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
     Body, ConstOperand, Operand, Rvalue, Terminator, TerminatorKind, VarDebugInfoContents,
 };
 use stable_mir::ty::{ClosureDef, FnDef, MirConst, RigidTy, TyKind, TypeAndMut, UintTy};
-use stable_mir::CrateDef;
 use std::collections::HashSet;
 use std::fmt::Debug;
 use tracing::{debug, trace};
@@ -420,10 +420,10 @@ impl FunctionWithContractPass {
             &mut mode_call,
             InsertPosition::Before,
         );
-        new_body.replace_terminator(
-            &mode_call,
-            Terminator { kind: TerminatorKind::Goto { target }, span },
-        );
+        new_body.replace_terminator(&mode_call, Terminator {
+            kind: TerminatorKind::Goto { target },
+            span,
+        });
 
         new_body.into()
     }
diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
index 5a026db525a7..845916af5181 100644
--- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
+++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
@@ -14,7 +14,7 @@ use crate::kani_middle::transform::body::{
 };
 use crate::kani_middle::transform::check_uninit::PointeeInfo;
 use crate::kani_middle::transform::check_uninit::{
-    get_mem_init_fn_def, mk_layout_operand, resolve_mem_init_fn, PointeeLayout,
+    PointeeLayout, get_mem_init_fn_def, mk_layout_operand, resolve_mem_init_fn,
 };
 use crate::kani_middle::transform::check_values::{build_limits, ty_validity_per_offset};
 use crate::kani_middle::transform::{TransformPass, TransformationType};
@@ -22,8 +22,8 @@ use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
-    BasicBlock, BinOp, Body, ConstOperand, Mutability, Operand, Place, Rvalue, Statement,
-    StatementKind, Terminator, TerminatorKind, UnwindAction, RETURN_LOCAL,
+    BasicBlock, BinOp, Body, ConstOperand, Mutability, Operand, Place, RETURN_LOCAL, Rvalue,
+    Statement, StatementKind, Terminator, TerminatorKind, UnwindAction,
 };
 use stable_mir::target::MachineInfo;
 use stable_mir::ty::{FnDef, MirConst, RigidTy, Ty, TyKind, UintTy};
diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs
index 2d963cd1d6eb..7d97a49f287a 100644
--- a/kani-compiler/src/kani_middle/transform/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/mod.rs
@@ -27,8 +27,8 @@ use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass};
 use crate::kani_queries::QueryDb;
 use dump_mir_pass::DumpMirPass;
 use rustc_middle::ty::TyCtxt;
-use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::mir::Body;
+use stable_mir::mir::mono::{Instance, MonoItem};
 use std::collections::HashMap;
 use std::fmt::Debug;
 
@@ -79,22 +79,16 @@ impl BodyTransformation {
         // would also make sense to check that the values are initialized before checking their
         // validity. In the future, it would be nice to have a mechanism to skip automatically
         // generated code for future instrumentation passes.
-        transformer.add_pass(
-            queries,
-            UninitPass {
-                // Since this uses demonic non-determinism under the hood, should not assume the assertion.
-                check_type: CheckType::new_assert(tcx),
-                mem_init_fn_cache: HashMap::new(),
-            },
-        );
-        transformer.add_pass(
-            queries,
-            IntrinsicGeneratorPass {
-                check_type,
-                mem_init_fn_cache: HashMap::new(),
-                arguments: queries.args().clone(),
-            },
-        );
+        transformer.add_pass(queries, UninitPass {
+            // Since this uses demonic non-determinism under the hood, should not assume the assertion.
+            check_type: CheckType::new_assert(tcx),
+            mem_init_fn_cache: HashMap::new(),
+        });
+        transformer.add_pass(queries, IntrinsicGeneratorPass {
+            check_type,
+            mem_init_fn_cache: HashMap::new(),
+            arguments: queries.args().clone(),
+        });
         transformer
     }
 
diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs
index 3dbd667c3943..09d6e1fe8520 100644
--- a/kani-compiler/src/kani_middle/transform/stubs.rs
+++ b/kani-compiler/src/kani_middle/transform/stubs.rs
@@ -9,11 +9,11 @@ use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
+use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::visit::{Location, MirVisitor};
 use stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind};
 use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
-use stable_mir::CrateDef;
 use std::collections::HashMap;
 use std::fmt::Debug;
 use tracing::{debug, trace};
diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs
index f5dd78ff86b0..d56877d11805 100644
--- a/kani-compiler/src/session.rs
+++ b/kani-compiler/src/session.rs
@@ -7,18 +7,18 @@ use crate::args::Arguments;
 use rustc_data_structures::sync::Lrc;
 use rustc_errors::emitter::Emitter;
 use rustc_errors::{
-    emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter, ColorConfig,
-    DiagInner,
+    ColorConfig, DiagInner, emitter::HumanReadableErrorType, fallback_fluent_bundle,
+    json::JsonEmitter,
 };
-use rustc_session::config::ErrorOutputType;
 use rustc_session::EarlyDiagCtxt;
+use rustc_session::config::ErrorOutputType;
 use rustc_span::source_map::FilePathMapping;
 use rustc_span::source_map::SourceMap;
 use std::io;
 use std::io::IsTerminal;
 use std::panic;
 use std::sync::LazyLock;
-use tracing_subscriber::{layer::SubscriberExt, EnvFilter, Registry};
+use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt};
 use tracing_tree::HierarchicalLayer;
 
 /// Environment variable used to control this session log tracing.
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index c3cfc113af64..72de44e36014 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -15,7 +15,7 @@ use crate::args::cargo::CargoTargetArgs;
 use crate::util::warning;
 use cargo::CargoCommonArgs;
 use clap::builder::{PossibleValue, TypedValueParser};
-use clap::{error::ContextKind, error::ContextValue, error::Error, error::ErrorKind, ValueEnum};
+use clap::{ValueEnum, error::ContextKind, error::ContextValue, error::Error, error::ErrorKind};
 use kani_metadata::CbmcSolver;
 use std::ffi::OsString;
 use std::path::PathBuf;
diff --git a/kani-driver/src/args_toml.rs b/kani-driver/src/args_toml.rs
index 37b38a425597..2fff01c4f5f9 100644
--- a/kani-driver/src/args_toml.rs
+++ b/kani-driver/src/args_toml.rs
@@ -1,14 +1,14 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use anyhow::{bail, Result};
+use anyhow::{Result, bail};
 use clap::Parser;
 use std::collections::BTreeMap;
 use std::ffi::OsString;
 use std::path::PathBuf;
 use std::process::Command;
-use toml::value::Table;
 use toml::Value;
+use toml::value::Table;
 
 /// Produce the list of arguments to pass to ourself (cargo-kani).
 ///
diff --git a/kani-driver/src/assess/metadata.rs b/kani-driver/src/assess/metadata.rs
index d555f1e4d309..14018541d0e5 100644
--- a/kani-driver/src/assess/metadata.rs
+++ b/kani-driver/src/assess/metadata.rs
@@ -15,11 +15,11 @@ use std::path::Path;
 use anyhow::Result;
 use serde::{Deserialize, Serialize};
 
+use super::AssessArgs;
 use super::table_builder::TableBuilder;
 use super::table_failure_reasons::FailureReasonsTableRow;
 use super::table_promising_tests::PromisingTestsTableRow;
 use super::table_unsupported_features::UnsupportedFeaturesTableRow;
-use super::AssessArgs;
 
 /// The structure of `.kani-assess-metadata.json` files. This is a the structure for both
 /// assess (standard) and scan. It it meant to hold results for one or more packages.
diff --git a/kani-driver/src/assess/mod.rs b/kani-driver/src/assess/mod.rs
index f5b2ccb63035..4ee82e48389c 100644
--- a/kani-driver/src/assess/mod.rs
+++ b/kani-driver/src/assess/mod.rs
@@ -1,8 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use self::metadata::{write_metadata, AssessMetadata};
-use anyhow::{bail, Result};
+use self::metadata::{AssessMetadata, write_metadata};
+use anyhow::{Result, bail};
 use kani_metadata::KaniMetadata;
 
 use crate::assess::table_builder::TableBuilder;
diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs
index ef33f91eb522..7ce29bb64b33 100644
--- a/kani-driver/src/assess/scan.rs
+++ b/kani-driver/src/assess/scan.rs
@@ -9,8 +9,8 @@ use std::time::Instant;
 use anyhow::Result;
 use cargo_metadata::Package;
 
-use crate::session::setup_cargo_command;
 use crate::session::KaniSession;
+use crate::session::setup_cargo_command;
 
 use super::metadata::AssessMetadata;
 use super::metadata::{aggregate_metadata, read_metadata};
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index ef289cead4c2..191b104a8c1c 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -2,11 +2,11 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::args::VerificationArgs;
-use crate::call_single_file::{to_rustc_arg, LibConfig};
+use crate::call_single_file::{LibConfig, to_rustc_arg};
 use crate::project::Artifact;
-use crate::session::{lib_folder, lib_no_core_folder, setup_cargo_command, KaniSession};
+use crate::session::{KaniSession, lib_folder, lib_no_core_folder, setup_cargo_command};
 use crate::util;
-use anyhow::{bail, Context, Result};
+use anyhow::{Context, Result, bail};
 use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
 use cargo_metadata::{
     Artifact as RustcArtifact, Message, Metadata, MetadataCommand, Package, Target,
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index bc4424aeb231..17e99bf17d0f 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -1,12 +1,12 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use anyhow::{bail, Result};
+use anyhow::{Result, bail};
 use kani_metadata::{CbmcSolver, HarnessMetadata};
 use regex::Regex;
 use rustc_demangle::demangle;
-use std::collections::btree_map::Entry;
 use std::collections::BTreeMap;
+use std::collections::btree_map::Entry;
 use std::ffi::OsString;
 use std::fmt::Write;
 use std::path::Path;
@@ -16,7 +16,7 @@ use std::time::{Duration, Instant};
 
 use crate::args::{OutputFormat, VerificationArgs};
 use crate::cbmc_output_parser::{
-    extract_results, process_cbmc_output, CheckStatus, Property, VerificationOutput,
+    CheckStatus, Property, VerificationOutput, extract_results, process_cbmc_output,
 };
 use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter};
 use crate::coverage::cov_results::{CoverageCheck, CoverageResults};
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 868d1adce636..63ca71d5b8d1 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -7,7 +7,7 @@ use std::ffi::OsString;
 use std::path::{Path, PathBuf};
 use std::process::Command;
 
-use crate::session::{lib_folder, KaniSession};
+use crate::session::{KaniSession, lib_folder};
 
 pub struct LibConfig {
     args: Vec<OsString>,
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index a0202169863c..145e0c9c63aa 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -22,127 +22,97 @@ static CBMC_ALT_DESCRIPTIONS: Lazy<CbmcAltDescriptions> = Lazy::new(|| {
     map.insert("error_label", vec![]);
     map.insert("division-by-zero", vec![("division by zero", None)]);
     map.insert("enum-range-check", vec![("enum range check", None)]);
-    map.insert(
-        "undefined-shift",
-        vec![
-            ("shift distance is negative", None),
-            ("shift distance too large", None),
-            ("shift operand is negative", None),
-            ("shift of non-integer type", None),
-        ],
-    );
-    map.insert(
-        "overflow",
-        vec![
-            ("result of signed mod is not representable", None),
-            ("arithmetic overflow on signed type conversion", None),
-            ("arithmetic overflow on signed division", None),
-            ("arithmetic overflow on signed unary minus", None),
-            ("arithmetic overflow on signed shl", None),
-            ("arithmetic overflow on unsigned unary minus", None),
-            ("arithmetic overflow on signed +", Some("arithmetic overflow on signed addition")),
-            ("arithmetic overflow on signed -", Some("arithmetic overflow on signed subtraction")),
-            (
-                "arithmetic overflow on signed *",
-                Some("arithmetic overflow on signed multiplication"),
-            ),
-            ("arithmetic overflow on unsigned +", Some("arithmetic overflow on unsigned addition")),
-            (
-                "arithmetic overflow on unsigned -",
-                Some("arithmetic overflow on unsigned subtraction"),
-            ),
-            (
-                "arithmetic overflow on unsigned *",
-                Some("arithmetic overflow on unsigned multiplication"),
-            ),
-            ("arithmetic overflow on floating-point typecast", None),
-            ("arithmetic overflow on floating-point division", None),
-            ("arithmetic overflow on floating-point addition", None),
-            ("arithmetic overflow on floating-point subtraction", None),
-            ("arithmetic overflow on floating-point multiplication", None),
-            ("arithmetic overflow on unsigned to signed type conversion", None),
-            ("arithmetic overflow on float to signed integer type conversion", None),
-            ("arithmetic overflow on signed to unsigned type conversion", None),
-            ("arithmetic overflow on unsigned to unsigned type conversion", None),
-            ("arithmetic overflow on float to unsigned integer type conversion", None),
-        ],
-    );
-    map.insert(
-        "NaN",
-        vec![
-            ("NaN on +", Some("NaN on addition")),
-            ("NaN on -", Some("NaN on subtraction")),
-            ("NaN on /", Some("NaN on division")),
-            ("NaN on *", Some("NaN on multiplication")),
-        ],
-    );
+    map.insert("undefined-shift", vec![
+        ("shift distance is negative", None),
+        ("shift distance too large", None),
+        ("shift operand is negative", None),
+        ("shift of non-integer type", None),
+    ]);
+    map.insert("overflow", vec![
+        ("result of signed mod is not representable", None),
+        ("arithmetic overflow on signed type conversion", None),
+        ("arithmetic overflow on signed division", None),
+        ("arithmetic overflow on signed unary minus", None),
+        ("arithmetic overflow on signed shl", None),
+        ("arithmetic overflow on unsigned unary minus", None),
+        ("arithmetic overflow on signed +", Some("arithmetic overflow on signed addition")),
+        ("arithmetic overflow on signed -", Some("arithmetic overflow on signed subtraction")),
+        ("arithmetic overflow on signed *", Some("arithmetic overflow on signed multiplication")),
+        ("arithmetic overflow on unsigned +", Some("arithmetic overflow on unsigned addition")),
+        ("arithmetic overflow on unsigned -", Some("arithmetic overflow on unsigned subtraction")),
+        (
+            "arithmetic overflow on unsigned *",
+            Some("arithmetic overflow on unsigned multiplication"),
+        ),
+        ("arithmetic overflow on floating-point typecast", None),
+        ("arithmetic overflow on floating-point division", None),
+        ("arithmetic overflow on floating-point addition", None),
+        ("arithmetic overflow on floating-point subtraction", None),
+        ("arithmetic overflow on floating-point multiplication", None),
+        ("arithmetic overflow on unsigned to signed type conversion", None),
+        ("arithmetic overflow on float to signed integer type conversion", None),
+        ("arithmetic overflow on signed to unsigned type conversion", None),
+        ("arithmetic overflow on unsigned to unsigned type conversion", None),
+        ("arithmetic overflow on float to unsigned integer type conversion", None),
+    ]);
+    map.insert("NaN", vec![
+        ("NaN on +", Some("NaN on addition")),
+        ("NaN on -", Some("NaN on subtraction")),
+        ("NaN on /", Some("NaN on division")),
+        ("NaN on *", Some("NaN on multiplication")),
+    ]);
     map.insert("pointer", vec![("same object violation", None)]);
-    map.insert(
-        "pointer_arithmetic",
-        vec![
-            ("pointer relation: deallocated dynamic object", None),
-            ("pointer relation: dead object", None),
-            ("pointer relation: pointer NULL", None),
-            ("pointer relation: pointer invalid", None),
-            ("pointer relation: pointer outside dynamic object bounds", None),
-            ("pointer relation: pointer outside object bounds", None),
-            ("pointer relation: invalid integer address", None),
-            ("pointer arithmetic: deallocated dynamic object", None),
-            ("pointer arithmetic: dead object", None),
-            ("pointer arithmetic: pointer NULL", None),
-            ("pointer arithmetic: pointer invalid", None),
-            ("pointer arithmetic: pointer outside dynamic object bounds", None),
-            ("pointer arithmetic: pointer outside object bounds", None),
-            ("pointer arithmetic: invalid integer address", None),
-        ],
-    );
-    map.insert(
-        "pointer_dereference",
-        vec![
-            (
-                "dereferenced function pointer must be",
-                Some("dereference failure: invalid function pointer"),
-            ),
-            ("dereference failure: pointer NULL", None),
-            ("dereference failure: pointer invalid", None),
-            ("dereference failure: deallocated dynamic object", None),
-            ("dereference failure: dead object", None),
-            ("dereference failure: pointer outside dynamic object bounds", None),
-            ("dereference failure: pointer outside object bounds", None),
-            ("dereference failure: invalid integer address", None),
-        ],
-    );
+    map.insert("pointer_arithmetic", vec![
+        ("pointer relation: deallocated dynamic object", None),
+        ("pointer relation: dead object", None),
+        ("pointer relation: pointer NULL", None),
+        ("pointer relation: pointer invalid", None),
+        ("pointer relation: pointer outside dynamic object bounds", None),
+        ("pointer relation: pointer outside object bounds", None),
+        ("pointer relation: invalid integer address", None),
+        ("pointer arithmetic: deallocated dynamic object", None),
+        ("pointer arithmetic: dead object", None),
+        ("pointer arithmetic: pointer NULL", None),
+        ("pointer arithmetic: pointer invalid", None),
+        ("pointer arithmetic: pointer outside dynamic object bounds", None),
+        ("pointer arithmetic: pointer outside object bounds", None),
+        ("pointer arithmetic: invalid integer address", None),
+    ]);
+    map.insert("pointer_dereference", vec![
+        (
+            "dereferenced function pointer must be",
+            Some("dereference failure: invalid function pointer"),
+        ),
+        ("dereference failure: pointer NULL", None),
+        ("dereference failure: pointer invalid", None),
+        ("dereference failure: deallocated dynamic object", None),
+        ("dereference failure: dead object", None),
+        ("dereference failure: pointer outside dynamic object bounds", None),
+        ("dereference failure: pointer outside object bounds", None),
+        ("dereference failure: invalid integer address", None),
+    ]);
     // These are very hard to understand without more context.
-    map.insert(
-        "pointer_primitives",
-        vec![
-            ("pointer invalid", None),
-            ("deallocated dynamic object", Some("pointer to deallocated dynamic object")),
-            ("dead object", Some("pointer to dead object")),
-            ("pointer outside dynamic object bounds", None),
-            ("pointer outside object bounds", None),
-            ("invalid integer address", None),
-        ],
-    );
-    map.insert(
-        "array_bounds",
-        vec![
-            ("lower bound", Some("index out of bounds")),
-            // This one is redundant:
-            // ("dynamic object upper bound", Some("access out of bounds")),
-            (
-                "upper bound",
-                Some("index out of bounds: the length is less than or equal to the given index"),
-            ),
-        ],
-    );
-    map.insert(
-        "bit_count",
-        vec![
-            ("count trailing zeros is undefined for value zero", None),
-            ("count leading zeros is undefined for value zero", None),
-        ],
-    );
+    map.insert("pointer_primitives", vec![
+        ("pointer invalid", None),
+        ("deallocated dynamic object", Some("pointer to deallocated dynamic object")),
+        ("dead object", Some("pointer to dead object")),
+        ("pointer outside dynamic object bounds", None),
+        ("pointer outside object bounds", None),
+        ("invalid integer address", None),
+    ]);
+    map.insert("array_bounds", vec![
+        ("lower bound", Some("index out of bounds")),
+        // This one is redundant:
+        // ("dynamic object upper bound", Some("access out of bounds")),
+        (
+            "upper bound",
+            Some("index out of bounds: the length is less than or equal to the given index"),
+        ),
+    ]);
+    map.insert("bit_count", vec![
+        ("count trailing zeros is undefined for value zero", None),
+        ("count leading zeros is undefined for value zero", None),
+    ]);
     map.insert("memory-leak", vec![("dynamically allocated memory never freed", None)]);
     // These pre-conditions should not print temporary variables since they are embedded in the libc implementation.
     // They are added via `__CPROVER_precondition`.
diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs
index c56694ad32fd..833fdbc02384 100644
--- a/kani-driver/src/concrete_playback/playback.rs
+++ b/kani-driver/src/concrete_playback/playback.rs
@@ -6,8 +6,8 @@
 use crate::args::common::Verbosity;
 use crate::args::playback_args::{CargoPlaybackArgs, KaniPlaybackArgs, MessageFormat};
 use crate::call_cargo::cargo_config_args;
-use crate::call_single_file::{base_rustc_flags, LibConfig};
-use crate::session::{lib_playback_folder, setup_cargo_command, InstallType};
+use crate::call_single_file::{LibConfig, base_rustc_flags};
+use crate::session::{InstallType, lib_playback_folder, setup_cargo_command};
 use crate::{session, util};
 use anyhow::Result;
 use std::ffi::OsString;
diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs
index 5faa6299a5d3..5c4076f13591 100644
--- a/kani-driver/src/concrete_playback/test_generator.rs
+++ b/kani-driver/src/concrete_playback/test_generator.rs
@@ -9,11 +9,11 @@ use crate::call_cbmc::VerificationResult;
 use crate::cbmc_output_parser::Property;
 use crate::session::KaniSession;
 use anyhow::{Context, Result};
-use concrete_vals_extractor::{extract_harness_values, ConcreteVal};
+use concrete_vals_extractor::{ConcreteVal, extract_harness_values};
 use kani_metadata::{HarnessKind, HarnessMetadata};
 use std::collections::hash_map::DefaultHasher;
 use std::ffi::OsString;
-use std::fs::{read_to_string, File};
+use std::fs::{File, read_to_string};
 use std::hash::{Hash, Hasher};
 use std::io::{BufRead, BufReader, Write};
 use std::path::Path;
@@ -500,10 +500,11 @@ mod tests {
     /// Check that the generated unit tests have the right formatting and indentation
     #[test]
     fn format_two_concrete_vals() {
-        let concrete_vals = [
-            ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() },
-            ConcreteVal { byte_arr: vec![0, 0, 0, 0, 0, 0, 0, 0], interp_val: "0l".to_string() },
-        ];
+        let concrete_vals =
+            [ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }, ConcreteVal {
+                byte_arr: vec![0, 0, 0, 0, 0, 0, 0, 0],
+                interp_val: "0l".to_string(),
+            }];
         let actual: Vec<_> = format_concrete_vals(&concrete_vals).collect();
         let expected = vec![
             format!("{:<8}// 0", " "),
@@ -597,10 +598,11 @@ mod tests {
 
     #[test]
     fn check_rustfmt_args_some_line_ranges() {
-        let file_line_ranges = [
-            FileLineRange { file: "file1".to_string(), line_range: None },
-            FileLineRange { file: "path/to/file2".to_string(), line_range: Some((1, 3)) },
-        ];
+        let file_line_ranges =
+            [FileLineRange { file: "file1".to_string(), line_range: None }, FileLineRange {
+                file: "path/to/file2".to_string(),
+                line_range: Some((1, 3)),
+            }];
         let args = rustfmt_args(&file_line_ranges);
         let expected: Vec<OsString> = [
             "--unstable-features",
diff --git a/kani-driver/src/coverage/cov_session.rs b/kani-driver/src/coverage/cov_session.rs
index bf6b34d3cd0b..60fa2f1c242f 100644
--- a/kani-driver/src/coverage/cov_session.rs
+++ b/kani-driver/src/coverage/cov_session.rs
@@ -5,10 +5,10 @@ use std::fs;
 use std::fs::File;
 use std::io::Write;
 
+use crate::KaniSession;
 use crate::harness_runner::HarnessResult;
 use crate::project::Project;
-use crate::KaniSession;
-use anyhow::{bail, Result};
+use anyhow::{Result, bail};
 
 impl KaniSession {
     /// Saves metadata required for coverage-related features.
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index 7e432932ab29..5a77a6a125a3 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use anyhow::{bail, Result};
+use anyhow::{Result, bail};
 use kani_metadata::{ArtifactType, HarnessMetadata};
 use rayon::prelude::*;
 use std::path::Path;
diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
index d3bd697d2ea4..e8ede555f180 100644
--- a/kani-driver/src/main.rs
+++ b/kani-driver/src/main.rs
@@ -5,9 +5,9 @@ use std::ffi::OsString;
 use std::process::ExitCode;
 
 use anyhow::Result;
-use time::{format_description, OffsetDateTime};
+use time::{OffsetDateTime, format_description};
 
-use args::{check_is_valid, CargoKaniSubcommand};
+use args::{CargoKaniSubcommand, check_is_valid};
 use args_toml::join_args;
 
 use crate::args::StandaloneSubcommand;
diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs
index 3f9cd8f2bf84..625d8b4bbcaa 100644
--- a/kani-driver/src/metadata.rs
+++ b/kani-driver/src/metadata.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use anyhow::{bail, Result};
+use anyhow::{Result, bail};
 use std::path::Path;
 use tracing::{debug, trace};
 
diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs
index e0d2d2edd139..363050958d61 100644
--- a/kani-driver/src/project.rs
+++ b/kani-driver/src/project.rs
@@ -9,7 +9,7 @@ use crate::session::KaniSession;
 use crate::util::crate_name;
 use anyhow::{Context, Result};
 use kani_metadata::{
-    artifact::convert_type, ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata,
+    ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata, artifact::convert_type,
 };
 use std::env::current_dir;
 use std::fs;
diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs
index 03cfb108e324..2df431eb4587 100644
--- a/kani-driver/src/session.rs
+++ b/kani-driver/src/session.rs
@@ -1,10 +1,10 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use crate::args::common::Verbosity;
 use crate::args::VerificationArgs;
+use crate::args::common::Verbosity;
 use crate::util::render_command;
-use anyhow::{bail, Context, Result};
+use anyhow::{Context, Result, bail};
 use std::io::IsTerminal;
 use std::io::Write;
 use std::path::{Path, PathBuf};
@@ -13,7 +13,7 @@ use std::sync::Mutex;
 use std::time::Instant;
 use strum_macros::Display;
 use tracing::level_filters::LevelFilter;
-use tracing_subscriber::{layer::SubscriberExt, EnvFilter, Registry};
+use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt};
 
 /// Environment variable used to control this session log tracing.
 /// This is the same variable used to control `kani-compiler` logs. Note that you can still control
diff --git a/kani_metadata/src/artifact.rs b/kani_metadata/src/artifact.rs
index 078cad14f679..12f8f9a49566 100644
--- a/kani_metadata/src/artifact.rs
+++ b/kani_metadata/src/artifact.rs
@@ -94,7 +94,7 @@ impl Deref for ArtifactType {
 
 #[cfg(test)]
 mod test {
-    use super::{convert_type, ArtifactType::*};
+    use super::{ArtifactType::*, convert_type};
     use std::path::PathBuf;
 
     #[test]
diff --git a/library/kani/src/futures.rs b/library/kani/src/futures.rs
index 637f24a80f6a..37cab17b0a5b 100644
--- a/library/kani/src/futures.rs
+++ b/library/kani/src/futures.rs
@@ -163,6 +163,7 @@ pub struct JoinHandle {
     index: usize,
 }
 
+#[allow(static_mut_refs)]
 impl Future for JoinHandle {
     type Output = ();
 
@@ -180,6 +181,7 @@ impl Future for JoinHandle {
 ///
 /// This function can only be called inside a future passed to [`block_on_with_spawn`].
 #[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")]
+#[allow(static_mut_refs)]
 pub fn spawn<F: Future<Output = ()> + Sync + 'static>(fut: F) -> JoinHandle {
     unsafe {
         if let Some(executor) = GLOBAL_EXECUTOR.as_mut() {
@@ -195,6 +197,7 @@ pub fn spawn<F: Future<Output = ()> + Sync + 'static>(fut: F) -> JoinHandle {
 ///
 /// Contrary to [`block_on`], this allows `spawn`ing other futures
 #[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")]
+#[allow(static_mut_refs)]
 pub fn block_on_with_spawn<F: Future<Output = ()> + Sync + 'static>(
     fut: F,
     scheduling_plan: impl SchedulingStrategy,
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index c3e9ae5497cc..053af760067b 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -44,7 +44,7 @@ pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
     unreachable!("Concrete playback does not work during verification")
 }
 
-pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin};
+pub use futures::{RoundRobin, block_on, block_on_with_spawn, spawn, yield_now};
 
 // Kani proc macros must be in a separate crate
 pub use kani_macros::*;
diff --git a/library/kani/src/vec.rs b/library/kani/src/vec.rs
index a3ec05a9c953..d9da65aa4537 100644
--- a/library/kani/src/vec.rs
+++ b/library/kani/src/vec.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::{any, any_where, Arbitrary};
+use crate::{Arbitrary, any, any_where};
 
 /// Generates an arbitrary vector whose length is at most MAX_LENGTH.
 pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>
diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs
index e89f6f089795..04b288069387 100644
--- a/library/kani_macros/src/derive.rs
+++ b/library/kani_macros/src/derive.rs
@@ -9,13 +9,13 @@
 //! struct S;
 //!
 //! ```
-use proc_macro2::{Ident, Span, TokenStream};
 use proc_macro_error2::abort;
+use proc_macro2::{Ident, Span, TokenStream};
 use quote::{quote, quote_spanned};
 use syn::spanned::Spanned;
 use syn::{
-    parse_macro_input, parse_quote, Data, DataEnum, DeriveInput, Fields, GenericParam, Generics,
-    Index,
+    Data, DataEnum, DeriveInput, Fields, GenericParam, Generics, Index, parse_macro_input,
+    parse_quote,
 };
 
 pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::TokenStream {
diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs
index 8a1d2d80f864..3e6c9d018422 100644
--- a/library/kani_macros/src/lib.rs
+++ b/library/kani_macros/src/lib.rs
@@ -409,7 +409,7 @@ mod sysroot {
     use {
         quote::{format_ident, quote},
         syn::parse::{Parse, ParseStream},
-        syn::{parse_macro_input, ItemFn},
+        syn::{ItemFn, parse_macro_input},
     };
 
     /// Annotate the harness with a #[kanitool::<name>] with optional arguments.
diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
index 8ad21e8a9c6b..5a9e12a62ae2 100644
--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
@@ -8,7 +8,7 @@ use proc_macro2::{Ident, Span, TokenStream};
 use quote::quote;
 use syn::{Expr, ItemFn, Stmt};
 
-use super::{helpers::*, ContractConditionsHandler, INTERNAL_RESULT_IDENT};
+use super::{ContractConditionsHandler, INTERNAL_RESULT_IDENT, helpers::*};
 
 impl<'a> ContractConditionsHandler<'a> {
     /// Generate initial contract.
diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs
index 314a5e74bc98..863cf882f063 100644
--- a/library/kani_macros/src/sysroot/contracts/check.rs
+++ b/library/kani_macros/src/sysroot/contracts/check.rs
@@ -6,11 +6,11 @@
 use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
 use quote::quote;
 use std::mem;
-use syn::{parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt};
+use syn::{Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt, parse_quote};
 
 use super::{
-    helpers::*, shared::build_ensures, ClosureType, ContractConditionsData,
-    ContractConditionsHandler, INTERNAL_RESULT_IDENT,
+    ClosureType, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
+    helpers::*, shared::build_ensures,
 };
 
 const WRAPPER_ARG: &str = "_wrapper_arg";
diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs
index 8db6218e2693..49d101dad32a 100644
--- a/library/kani_macros/src/sysroot/contracts/helpers.rs
+++ b/library/kani_macros/src/sysroot/contracts/helpers.rs
@@ -9,8 +9,8 @@ use proc_macro2::{Ident, Span};
 use std::borrow::Cow;
 use syn::spanned::Spanned;
 use syn::{
-    parse_quote, Attribute, Expr, ExprBlock, ExprCall, ExprPath, Local, LocalInit, PatIdent, Path,
-    Stmt,
+    Attribute, Expr, ExprBlock, ExprCall, ExprPath, Local, LocalInit, PatIdent, Path, Stmt,
+    parse_quote,
 };
 
 /// If an explicit return type was provided it is returned, otherwise `()`.
diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs
index 50c63173b601..bd06139b27f5 100644
--- a/library/kani_macros/src/sysroot/contracts/initialize.rs
+++ b/library/kani_macros/src/sysroot/contracts/initialize.rs
@@ -8,9 +8,9 @@ use proc_macro2::TokenStream as TokenStream2;
 use syn::ItemFn;
 
 use super::{
-    helpers::{chunks_by, is_token_stream_2_comma, matches_path},
     ContractConditionsData, ContractConditionsHandler, ContractConditionsType,
     ContractFunctionState,
+    helpers::{chunks_by, is_token_stream_2_comma, matches_path},
 };
 
 impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState {
diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs
index 281960bf041b..41be536ffb6d 100644
--- a/library/kani_macros/src/sysroot/contracts/mod.rs
+++ b/library/kani_macros/src/sysroot/contracts/mod.rs
@@ -395,7 +395,7 @@
 use proc_macro::TokenStream;
 use proc_macro2::{Ident, TokenStream as TokenStream2};
 use quote::quote;
-use syn::{parse_macro_input, parse_quote, Expr, ExprClosure, ItemFn};
+use syn::{Expr, ExprClosure, ItemFn, parse_macro_input, parse_quote};
 
 mod bootstrap;
 mod check;
diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs
index 71913e630622..b28e178bea6d 100644
--- a/library/kani_macros/src/sysroot/contracts/replace.rs
+++ b/library/kani_macros/src/sysroot/contracts/replace.rs
@@ -9,9 +9,9 @@ use std::mem;
 use syn::Stmt;
 
 use super::{
+    ClosureType, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
     helpers::*,
     shared::{build_ensures, try_as_result_assign},
-    ClosureType, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
 };
 
 impl<'a> ContractConditionsHandler<'a> {
diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs
index f189a9f98b0c..d7e77ee2a8d4 100644
--- a/library/kani_macros/src/sysroot/contracts/shared.rs
+++ b/library/kani_macros/src/sysroot/contracts/shared.rs
@@ -12,7 +12,7 @@ use std::collections::HashMap;
 use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
 use quote::quote;
 use std::hash::{DefaultHasher, Hash, Hasher};
-use syn::{spanned::Spanned, visit_mut::VisitMut, Expr, ExprCall, ExprClosure, ExprPath, Path};
+use syn::{Expr, ExprCall, ExprClosure, ExprPath, Path, spanned::Spanned, visit_mut::VisitMut};
 
 use super::INTERNAL_RESULT_IDENT;
 
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 8280b9442a9b..28cedff1d1de 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-09-20"
+channel = "nightly-2024-09-23"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/rustfmt.toml b/rustfmt.toml
index 95988ef7f52a..44cbfe4a3dc9 100644
--- a/rustfmt.toml
+++ b/rustfmt.toml
@@ -3,7 +3,7 @@
 
 # Run rustfmt with this config (it should be picked up automatically).
 edition = "2021"
-version = "Two"
+style_edition = "2024"
 use_small_heuristics = "Max"
 merge_derives = false
 
diff --git a/src/cmd.rs b/src/cmd.rs
index 77204f092e74..1ab9216a4d46 100644
--- a/src/cmd.rs
+++ b/src/cmd.rs
@@ -7,7 +7,7 @@
 use std::ffi::OsString;
 use std::process::Command;
 
-use anyhow::{bail, Context, Result};
+use anyhow::{Context, Result, bail};
 
 /// Helper trait to fallibly run commands
 pub trait AutoRun {
diff --git a/src/lib.rs b/src/lib.rs
index 0015829f61d3..f24163d3213c 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -22,7 +22,7 @@ use std::path::{Path, PathBuf};
 use std::process::Command;
 use std::{env, fs};
 
-use anyhow::{bail, Context, Result};
+use anyhow::{Context, Result, bail};
 
 /// Effectively the entry point (i.e. `main` function) for both our proxy binaries.
 /// `bin` should be either `kani` or `cargo-kani`
diff --git a/src/os_hacks.rs b/src/os_hacks.rs
index ca064a662901..8d3a20575d7d 100644
--- a/src/os_hacks.rs
+++ b/src/os_hacks.rs
@@ -8,7 +8,7 @@
 use std::path::Path;
 use std::process::Command;
 
-use anyhow::{bail, Context, Result};
+use anyhow::{Context, Result, bail};
 use os_info::Info;
 
 use crate::cmd::AutoRun;
diff --git a/src/setup.rs b/src/setup.rs
index 58387f7031b7..eb1227269ccc 100644
--- a/src/setup.rs
+++ b/src/setup.rs
@@ -8,7 +8,7 @@ use std::ffi::OsString;
 use std::path::{Path, PathBuf};
 use std::process::Command;
 
-use anyhow::{bail, Context, Result};
+use anyhow::{Context, Result, bail};
 
 use crate::cmd::AutoRun;
 use crate::os_hacks;
diff --git a/tests/cargo-kani/percent-encoding/src/lib.rs b/tests/cargo-kani/percent-encoding/src/lib.rs
index 8da898139aa8..e9667b7cb375 100644
--- a/tests/cargo-kani/percent-encoding/src/lib.rs
+++ b/tests/cargo-kani/percent-encoding/src/lib.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use percent_encoding::{utf8_percent_encode, NON_ALPHANUMERIC};
+use percent_encoding::{NON_ALPHANUMERIC, utf8_percent_encode};
 
 #[kani::proof]
 pub fn check_encoding() {
diff --git a/tests/cargo-kani/small-vec/src/lib.rs b/tests/cargo-kani/small-vec/src/lib.rs
index 45b07a345285..dbf9d7f9065c 100644
--- a/tests/cargo-kani/small-vec/src/lib.rs
+++ b/tests/cargo-kani/small-vec/src/lib.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use smallvec::{smallvec, SmallVec};
+use smallvec::{SmallVec, smallvec};
 
 #[kani::proof]
 #[kani::unwind(4)]
diff --git a/tests/cargo-kani/stubbing-use-as-foreign/src/lib.rs b/tests/cargo-kani/stubbing-use-as-foreign/src/lib.rs
index 34d29bb3423d..bac3b9b1390c 100644
--- a/tests/cargo-kani/stubbing-use-as-foreign/src/lib.rs
+++ b/tests/cargo-kani/stubbing-use-as-foreign/src/lib.rs
@@ -5,9 +5,9 @@
 //! YYY;`) referring to external code when resolving paths in `kani::stub`
 //! attributes.
 
+use other_crate::MyType as MyFavoriteType;
 use other_crate::inner_mod::magic_number42 as forty_two;
 use other_crate::magic_number13 as thirteen;
-use other_crate::MyType as MyFavoriteType;
 
 #[kani::proof]
 #[kani::stub(zero, thirteen)]
diff --git a/tests/cargo-kani/stubbing-use-foreign/src/lib.rs b/tests/cargo-kani/stubbing-use-foreign/src/lib.rs
index 07e86207a944..def0ce5a73eb 100644
--- a/tests/cargo-kani/stubbing-use-foreign/src/lib.rs
+++ b/tests/cargo-kani/stubbing-use-foreign/src/lib.rs
@@ -4,9 +4,9 @@
 //! This tests whether we take into account use statements (`use XXX;`)
 //! referring to external code when resolving paths in `kani::stub` attributes.
 
+use other_crate::MyType;
 use other_crate::inner_mod::magic_number42;
 use other_crate::magic_number13;
-use other_crate::MyType;
 
 #[kani::proof]
 #[kani::stub(zero, magic_number13)]
diff --git a/tests/cargo-kani/vecdeque-cve/src/harness.rs b/tests/cargo-kani/vecdeque-cve/src/harness.rs
index 5c36450ee36a..f8ec8f5fdbde 100644
--- a/tests/cargo-kani/vecdeque-cve/src/harness.rs
+++ b/tests/cargo-kani/vecdeque-cve/src/harness.rs
@@ -27,8 +27,8 @@ const MAX_CAPACITY: usize = usize::MAX >> 2;
 
 /// This module uses a version of VecDeque that includes the CVE fix.
 mod fixed_proofs {
-    use crate::fixed::VecDeque;
     use crate::MAX_CAPACITY;
+    use crate::fixed::VecDeque;
 
     /// Minimal example that we no longer expect to fail
     #[kani::proof]
@@ -98,8 +98,8 @@ mod fixed_proofs {
 
 mod cve_proofs {
     // Modified version of vec_deque with reserve issue.
-    use crate::cve::VecDeque;
     use crate::MAX_CAPACITY;
+    use crate::cve::VecDeque;
 
     /// Minimal example that we expect to fail
     #[kani::proof]
diff --git a/tests/expected/dealloc/stack/test.rs b/tests/expected/dealloc/stack/test.rs
index 87da636d8916..a4b1e3f481e3 100644
--- a/tests/expected/dealloc/stack/test.rs
+++ b/tests/expected/dealloc/stack/test.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use std::alloc::{dealloc, Layout};
+use std::alloc::{Layout, dealloc};
 
 // This test checks that Kani flags the deallocation of a stack-allocated
 // variable
diff --git a/tests/expected/realloc/null/main.rs b/tests/expected/realloc/null/main.rs
index 668ad4f84c2f..6f5a3b8bd2ab 100644
--- a/tests/expected/realloc/null/main.rs
+++ b/tests/expected/realloc/null/main.rs
@@ -3,7 +3,7 @@
 
 // Calling realloc with a null pointer fails
 
-use std::alloc::{realloc, Layout};
+use std::alloc::{Layout, realloc};
 
 #[kani::proof]
 fn main() {
diff --git a/tests/expected/realloc/shrink/main.rs b/tests/expected/realloc/shrink/main.rs
index 7c4bd377fea7..d7b31244a9f7 100644
--- a/tests/expected/realloc/shrink/main.rs
+++ b/tests/expected/realloc/shrink/main.rs
@@ -4,7 +4,7 @@
 // Use realloc to shrink the size of the allocated block and make sure
 // out-of-bound accesses result in verification failure
 
-use std::alloc::{alloc, dealloc, realloc, Layout};
+use std::alloc::{Layout, alloc, dealloc, realloc};
 
 #[kani::proof]
 fn main() {
diff --git a/tests/expected/realloc/zero_size/main.rs b/tests/expected/realloc/zero_size/main.rs
index 3e347af7512f..620ce17fdd2d 100644
--- a/tests/expected/realloc/zero_size/main.rs
+++ b/tests/expected/realloc/zero_size/main.rs
@@ -3,7 +3,7 @@
 
 // Calling realloc with a size of zero fails
 
-use std::alloc::{alloc, realloc, Layout};
+use std::alloc::{Layout, alloc, realloc};
 
 #[kani::proof]
 fn main() {
diff --git a/tests/expected/shadow/uninit_array/test.rs b/tests/expected/shadow/uninit_array/test.rs
index 8a9536e5a8e8..046d0f9f551f 100644
--- a/tests/expected/shadow/uninit_array/test.rs
+++ b/tests/expected/shadow/uninit_array/test.rs
@@ -6,7 +6,7 @@
 // It checks that shadow memory can be used to track whether a memory location
 // is initialized.
 
-use std::alloc::{alloc, dealloc, Layout};
+use std::alloc::{Layout, alloc, dealloc};
 
 static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
 
diff --git a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs
index 318f234c31be..d4e4c4b758da 100644
--- a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs
+++ b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Z uninit-checks
 
-use std::alloc::{alloc, Layout};
+use std::alloc::{Layout, alloc};
 use std::slice::from_raw_parts;
 
 /// Checks that Kani catches an attempt to form a slice from uninitialized memory.
diff --git a/tests/expected/uninit/atomic/atomic.rs b/tests/expected/uninit/atomic/atomic.rs
index 63c85af41a3f..78b9dd2fdea0 100644
--- a/tests/expected/uninit/atomic/atomic.rs
+++ b/tests/expected/uninit/atomic/atomic.rs
@@ -4,7 +4,7 @@
 
 #![feature(core_intrinsics)]
 
-use std::alloc::{alloc, Layout};
+use std::alloc::{Layout, alloc};
 use std::sync::atomic::{AtomicU8, Ordering};
 
 // Checks if memory initialization checks correctly fail when uninitialized memory is passed to
diff --git a/tests/expected/uninit/intrinsics/intrinsics.rs b/tests/expected/uninit/intrinsics/intrinsics.rs
index b023853b2fbc..33d5e72b1da9 100644
--- a/tests/expected/uninit/intrinsics/intrinsics.rs
+++ b/tests/expected/uninit/intrinsics/intrinsics.rs
@@ -5,7 +5,7 @@
 
 #![feature(core_intrinsics)]
 
-use std::alloc::{alloc, alloc_zeroed, Layout};
+use std::alloc::{Layout, alloc, alloc_zeroed};
 use std::intrinsics::*;
 
 #[kani::proof]
diff --git a/tests/kani/AsyncAwait/spawn.rs b/tests/kani/AsyncAwait/spawn.rs
index 76583f10d615..fa203b2a5c12 100644
--- a/tests/kani/AsyncAwait/spawn.rs
+++ b/tests/kani/AsyncAwait/spawn.rs
@@ -7,8 +7,8 @@
 //! This file tests the executor and spawn infrastructure from the Kani library.
 
 use std::sync::{
-    atomic::{AtomicI64, Ordering},
     Arc,
+    atomic::{AtomicI64, Ordering},
 };
 
 #[kani::proof(schedule = kani::RoundRobin::default())]
diff --git a/tests/kani/Coroutines/issue-1593.rs b/tests/kani/Coroutines/issue-1593.rs
index 9028dadad3d3..b85aefba9378 100644
--- a/tests/kani/Coroutines/issue-1593.rs
+++ b/tests/kani/Coroutines/issue-1593.rs
@@ -8,8 +8,8 @@
 // in the context of vtables.
 
 use std::sync::{
-    atomic::{AtomicI64, Ordering},
     Arc,
+    atomic::{AtomicI64, Ordering},
 };
 
 #[kani::proof]
diff --git a/tests/kani/FatPointers/boxmuttrait.rs b/tests/kani/FatPointers/boxmuttrait.rs
index aa965f56c71e..a9469d7273f1 100644
--- a/tests/kani/FatPointers/boxmuttrait.rs
+++ b/tests/kani/FatPointers/boxmuttrait.rs
@@ -9,7 +9,7 @@
 #![feature(ptr_metadata)]
 
 use std::any::Any;
-use std::io::{sink, Write};
+use std::io::{Write, sink};
 use std::ptr::DynMetadata;
 
 include!("../Helpers/vtable_utils_ignore.rs");
diff --git a/tests/kani/FatPointers/boxmuttrait_fail.rs b/tests/kani/FatPointers/boxmuttrait_fail.rs
index 4d4dc6fc8384..35d05a58c6f8 100644
--- a/tests/kani/FatPointers/boxmuttrait_fail.rs
+++ b/tests/kani/FatPointers/boxmuttrait_fail.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-verify-fail
 
-use std::io::{sink, Write};
+use std::io::{Write, sink};
 
 #[kani::proof]
 fn main() {
diff --git a/tests/kani/Intrinsics/Atomic/Stable/Fence/main.rs b/tests/kani/Intrinsics/Atomic/Stable/Fence/main.rs
index a119364f9b42..6ea70ab3b830 100644
--- a/tests/kani/Intrinsics/Atomic/Stable/Fence/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Stable/Fence/main.rs
@@ -4,7 +4,7 @@
 // Check that `atomic_fence` and other variants (stable version) can be
 // processed.
 
-use std::sync::atomic::{fence, Ordering};
+use std::sync::atomic::{Ordering, fence};
 
 #[kani::proof]
 fn main() {
diff --git a/tests/kani/Intrinsics/RawEq/uninit_eq.rs b/tests/kani/Intrinsics/RawEq/uninit_eq.rs
index 9e7f81dfaef1..390e0f774a4a 100644
--- a/tests/kani/Intrinsics/RawEq/uninit_eq.rs
+++ b/tests/kani/Intrinsics/RawEq/uninit_eq.rs
@@ -6,7 +6,7 @@
 // uninitialized
 #![feature(core_intrinsics)]
 use std::intrinsics::raw_eq;
-use std::mem::{zeroed, MaybeUninit};
+use std::mem::{MaybeUninit, zeroed};
 
 #[kani::proof]
 fn main() {
diff --git a/tests/kani/Intrinsics/RawEq/uninit_ne.rs b/tests/kani/Intrinsics/RawEq/uninit_ne.rs
index 0f0642976671..73b5715b4846 100644
--- a/tests/kani/Intrinsics/RawEq/uninit_ne.rs
+++ b/tests/kani/Intrinsics/RawEq/uninit_ne.rs
@@ -6,7 +6,7 @@
 // is uninitialized
 #![feature(core_intrinsics)]
 use std::intrinsics::raw_eq;
-use std::mem::{zeroed, MaybeUninit};
+use std::mem::{MaybeUninit, zeroed};
 
 #[kani::proof]
 fn main() {
diff --git a/tests/kani/Realloc/two_reallocs.rs b/tests/kani/Realloc/two_reallocs.rs
index 449e00cce56d..dc7b5ec3cd87 100644
--- a/tests/kani/Realloc/two_reallocs.rs
+++ b/tests/kani/Realloc/two_reallocs.rs
@@ -3,7 +3,7 @@
 
 // Perform two reallocs in a row and make sure the data is properly copied
 
-use std::alloc::{alloc, dealloc, realloc, Layout};
+use std::alloc::{Layout, alloc, dealloc, realloc};
 
 #[kani::proof]
 fn main() {
diff --git a/tests/kani/Stubbing/resolve_use.rs b/tests/kani/Stubbing/resolve_use.rs
index ac1f6f7325f8..20c5faddfdc6 100644
--- a/tests/kani/Stubbing/resolve_use.rs
+++ b/tests/kani/Stubbing/resolve_use.rs
@@ -20,8 +20,8 @@ impl MyType {
 
 mod my_mod {
     use self::inner_mod::magic_number42;
-    use super::magic_number13;
     use super::MyType;
+    use super::magic_number13;
 
     mod inner_mod {
         pub fn magic_number42() -> u32 {
diff --git a/tests/kani/Stubbing/resolve_use_as.rs b/tests/kani/Stubbing/resolve_use_as.rs
index 790e26e575e9..5f55b8f7ac59 100644
--- a/tests/kani/Stubbing/resolve_use_as.rs
+++ b/tests/kani/Stubbing/resolve_use_as.rs
@@ -20,8 +20,8 @@ impl MyType {
 
 mod my_mod {
     use self::inner_mod::magic_number42 as forty_two;
-    use super::magic_number13 as thirteen;
     use super::MyType as MyFavoriteType;
+    use super::magic_number13 as thirteen;
 
     mod inner_mod {
         pub fn magic_number42() -> u32 {
diff --git a/tests/kani/Uninit/alloc-to-slice.rs b/tests/kani/Uninit/alloc-to-slice.rs
index 863d3b40b390..6f235fa41b51 100644
--- a/tests/kani/Uninit/alloc-to-slice.rs
+++ b/tests/kani/Uninit/alloc-to-slice.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Z uninit-checks
 
-use std::alloc::{alloc, Layout};
+use std::alloc::{Layout, alloc};
 
 #[kani::proof]
 fn alloc_to_slice() {
diff --git a/tests/kani/Uninit/alloc-zeroed-to-slice.rs b/tests/kani/Uninit/alloc-zeroed-to-slice.rs
index d00ca4c6abff..1e463b3227a0 100644
--- a/tests/kani/Uninit/alloc-zeroed-to-slice.rs
+++ b/tests/kani/Uninit/alloc-zeroed-to-slice.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Z uninit-checks
 
-use std::alloc::{alloc_zeroed, Layout};
+use std::alloc::{Layout, alloc_zeroed};
 use std::slice::from_raw_parts;
 
 #[kani::proof]
diff --git a/tests/perf/hashset/src/lib.rs b/tests/perf/hashset/src/lib.rs
index e2f1fc16666a..c9a3c01f93de 100644
--- a/tests/perf/hashset/src/lib.rs
+++ b/tests/perf/hashset/src/lib.rs
@@ -3,7 +3,7 @@
 // kani-flags: -Z stubbing
 //! Try to verify HashSet basic behavior.
 
-use std::collections::{hash_map::RandomState, HashSet};
+use std::collections::{HashSet, hash_map::RandomState};
 use std::mem::{size_of, size_of_val, transmute};
 
 #[allow(dead_code)]
diff --git a/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs b/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs
index 891a97fd8c22..008e7d132f10 100644
--- a/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs
+++ b/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Z uninit-checks
 
-use std::alloc::{alloc_zeroed, Layout};
+use std::alloc::{Layout, alloc_zeroed};
 use std::slice::from_raw_parts;
 
 #[kani::proof]
diff --git a/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs b/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs
index 16b87cfadf5a..d013af942b9b 100644
--- a/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs
+++ b/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs
@@ -9,7 +9,7 @@
 #![warn(rust_2018_idioms)]
 #![cfg(feature = "full")]
 
-use tokio::io::{duplex, AsyncReadExt, AsyncWriteExt};
+use tokio::io::{AsyncReadExt, AsyncWriteExt, duplex};
 
 #[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
diff --git a/tests/slow/tokio-proofs/src/tokio/support/panic.rs b/tests/slow/tokio-proofs/src/tokio/support/panic.rs
index 12ae92a521e4..b35fde0ecdd7 100644
--- a/tests/slow/tokio-proofs/src/tokio/support/panic.rs
+++ b/tests/slow/tokio-proofs/src/tokio/support/panic.rs
@@ -6,7 +6,7 @@
 // Original copyright tokio contributors.
 // origin: tokio/tests/support
 
-use parking_lot::{const_mutex, Mutex};
+use parking_lot::{Mutex, const_mutex};
 use std::panic;
 use std::sync::Arc;
 
diff --git a/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs b/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs
index 39cb46077626..72c4d486daf8 100644
--- a/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs
+++ b/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs
@@ -7,7 +7,7 @@
 // origin: tokio-stream/tests/ at commit b2ada60e701d5c9e6644cf8fc42a100774f8e23f
 
 use crate::tokio_stream::support::mpsc;
-use tokio_stream::{self as stream, pending, Stream, StreamExt, StreamMap};
+use tokio_stream::{self as stream, Stream, StreamExt, StreamMap, pending};
 use tokio_test::{assert_ok, assert_pending, assert_ready, task};
 
 use std::pin::Pin;
diff --git a/tests/slow/tokio-proofs/src/tokio_test/block_on.rs b/tests/slow/tokio-proofs/src/tokio_test/block_on.rs
index 62b5c0a514a2..3bf00ac0a5a7 100644
--- a/tests/slow/tokio-proofs/src/tokio_test/block_on.rs
+++ b/tests/slow/tokio-proofs/src/tokio_test/block_on.rs
@@ -8,7 +8,7 @@
 
 #![warn(rust_2018_idioms)]
 
-use tokio::time::{sleep_until, Duration, Instant};
+use tokio::time::{Duration, Instant, sleep_until};
 use tokio_test::block_on;
 
 #[cfg(disabled)] // because epoll is missing
diff --git a/tests/std-checks/std/src/sync/atomic.rs b/tests/std-checks/std/src/sync/atomic.rs
index 85c9a3380775..f6fc822bf40a 100644
--- a/tests/std-checks/std/src/sync/atomic.rs
+++ b/tests/std-checks/std/src/sync/atomic.rs
@@ -3,7 +3,7 @@
 
 extern crate kani;
 
-use std::sync::atomic::{AtomicU16, AtomicU32, AtomicU64, AtomicU8, AtomicUsize};
+use std::sync::atomic::{AtomicU8, AtomicU16, AtomicU32, AtomicU64, AtomicUsize};
 
 /// Create wrapper functions to standard library functions that contains their contract.
 pub mod contracts {
diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs
index 2c181d69d6e5..7000ddb045a7 100644
--- a/tools/build-kani/src/main.rs
+++ b/tools/build-kani/src/main.rs
@@ -11,7 +11,7 @@ mod parser;
 mod sysroot;
 
 use crate::sysroot::{build_bin, build_lib, kani_no_core_lib, kani_playback_lib, kani_sysroot_lib};
-use anyhow::{bail, Result};
+use anyhow::{Result, bail};
 use clap::Parser;
 use std::{ffi::OsString, path::Path, process::Command};
 
diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs
index ca42fea3f441..edd2a0973a83 100644
--- a/tools/build-kani/src/sysroot.rs
+++ b/tools/build-kani/src/sysroot.rs
@@ -11,8 +11,8 @@
 //!
 //! Note: We don't cross-compile. Target is the same as the host.
 
-use crate::{cp, AutoRun};
-use anyhow::{bail, format_err, Result};
+use crate::{AutoRun, cp};
+use anyhow::{Result, bail, format_err};
 use cargo_metadata::{Artifact, Message};
 use std::ffi::OsStr;
 use std::fs;
diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs
index d5c4ccf3c116..0ff106c92de3 100644
--- a/tools/compiletest/src/common.rs
+++ b/tools/compiletest/src/common.rs
@@ -10,8 +10,8 @@ use std::path::{Path, PathBuf};
 use std::str::FromStr;
 
 use std::time::Duration;
-use test::test::TestTimeOptions;
 use test::ColorConfig;
+use test::test::TestTimeOptions;
 
 #[derive(Clone, Copy, Eq, PartialEq, Debug)]
 pub enum Mode {
diff --git a/tools/compiletest/src/header.rs b/tools/compiletest/src/header.rs
index afbee19e6ade..f49d4f64ce47 100644
--- a/tools/compiletest/src/header.rs
+++ b/tools/compiletest/src/header.rs
@@ -4,8 +4,8 @@
 // See GitHub history for details.
 
 use std::fs::File;
-use std::io::prelude::*;
 use std::io::BufReader;
+use std::io::prelude::*;
 use std::path::Path;
 
 use tracing::*;
diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs
index dd1284d7a3c9..9027e30121f8 100644
--- a/tools/compiletest/src/main.rs
+++ b/tools/compiletest/src/main.rs
@@ -10,8 +10,8 @@
 
 extern crate test;
 
-use crate::common::{output_base_dir, output_relative_path};
 use crate::common::{Config, Mode, TestPaths};
+use crate::common::{output_base_dir, output_relative_path};
 use crate::util::{logv, print_msg, top_level};
 use getopts::Options;
 use std::env;
@@ -21,8 +21,8 @@ use std::io::{self};
 use std::path::{Path, PathBuf};
 use std::str::FromStr;
 use std::time::{Duration, SystemTime};
-use test::test::TestTimeOptions;
 use test::ColorConfig;
+use test::test::TestTimeOptions;
 use tracing::*;
 use walkdir::WalkDir;
 
diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs
index c6575db17819..6e6425d086c3 100644
--- a/tools/compiletest/src/runtest.rs
+++ b/tools/compiletest/src/runtest.rs
@@ -6,11 +6,11 @@
 // ignore-tidy-filelength
 
 use crate::common::KaniFailStep;
-use crate::common::{output_base_dir, output_base_name};
 use crate::common::{
     CargoCoverage, CargoKani, CargoKaniTest, CoverageBased, Exec, Expected, Kani, KaniFixme, Stub,
 };
 use crate::common::{Config, TestPaths};
+use crate::common::{output_base_dir, output_base_name};
 use crate::header::TestProps;
 use crate::read2::read2;
 use crate::util::logv;
diff --git a/tools/scanner/src/analysis.rs b/tools/scanner/src/analysis.rs
index b32627939bf5..e0f65929ffdd 100644
--- a/tools/scanner/src/analysis.rs
+++ b/tools/scanner/src/analysis.rs
@@ -7,7 +7,7 @@ use crate::info;
 use csv::WriterBuilder;
 use graph_cycles::Cycles;
 use petgraph::graph::Graph;
-use serde::{ser::SerializeStruct, Serialize, Serializer};
+use serde::{Serialize, Serializer, ser::SerializeStruct};
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef};
 use stable_mir::mir::{