Clippy fixes

model-checking · Dec 19, 2023 · fb4c470 · fb4c470
1 parent 3e51204
commit fb4c470
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 29 deletions.
diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
@@ -31,7 +31,7 @@ use tracing::{debug, debug_span, trace};
 use super::kani_intrinsic::get_kani_intrinsic;
 use super::smt_builtins::{smt_builtin_binop, SmtBvBuiltin};
 
-const UNBOUNDED_ARRAY: &'static str = "$Array";
+const UNBOUNDED_ARRAY: &str = "$Array";
 
 /// A context that provides the main methods for translating MIR constructs to
 /// Boogie and stores what has been codegen so far
@@ -520,34 +520,7 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
  return expr.clone();
  }
  //let local_ty = self.mir.local_decls()[place.local].ty;
- let local = self.codegen_local(place.local);
- local
- //place.projection.iter().fold(local, |place, proj| {
- // match proj {
- // ProjectionElem::Index(i) => {
- // let index = self.codegen_local(i);
- // Expr::Index { base: Box::new(place), index: Box::new(index) }
- // }
- // ProjectionElem::Field(f, _t) => {
- // debug!(ty=?local_ty, "codegen_place_fold");
- // match local_ty.kind() {
- // ty::Adt(def, _args) => {
- // let field_name = def.non_enum_variant().fields[f].name.to_string();
- // Expr::Field { base: Box::new(place), field: field_name }
- // }
- // ty::Tuple(_types) => {
- // // TODO: handle tuples
- // place
- // }
- // _ => todo!(),
- // }
- // }
- // _ => {
- // // TODO: handle
- // place
- // }
- // }
- //})
+ self.codegen_local(place.local)
  }
 
  fn codegen_local(&self, local: Local) -> Expr {

diff --git a/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs b/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs
@@ -18,6 +18,7 @@ use tracing::debug;
 
 // TODO: move this enum up to `kani_middle`
 #[derive(Debug, Clone, PartialEq, Eq, EnumString, EnumVariantNames)]
+#[allow(clippy::enum_variant_names)]
 pub enum KaniIntrinsic {
  /// Kani assert statement (`kani::assert`)
  KaniAssert,