Hopefully fixing clippy suggestions

model-checking · Jun 22, 2023 · 03eab7c · 03eab7c
1 parent 24ea785
commit 03eab7c
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 6 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -251,7 +251,7 @@ impl<'tcx> GotocCtx<'tcx> {
         use rustc_middle::mir;
         let mut handle_contract_expr = |instance| {
             let mir = self.current_fn().mir();
-            assert!(!mir.spread_arg.is_some());
+            assert!(mir.spread_arg.is_none());
             let func_expr = self.codegen_func_expr(instance, None);
             let mut mir_arguments: Vec<_> =
                 std::iter::successors(Some(mir::RETURN_PLACE + 1), |i| Some(*i + 1))

diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -70,6 +70,8 @@ pub struct GotocCodegenBackend {
     queries: Arc<Mutex<QueryDb>>,
 }
 
+type MonoContract<'tcx> = GFnContract<ty::Instance<'tcx>>;
+
 impl GotocCodegenBackend {
     pub fn new(queries: Arc<Mutex<QueryDb>>) -> Self {
         GotocCodegenBackend { queries }
@@ -82,7 +84,7 @@ impl GotocCodegenBackend {
         starting_items: &[MonoItem<'tcx>],
         symtab_goto: &Path,
         machine_model: &MachineModel,
-    ) -> (GotocCtx<'tcx>, Vec<(MonoItem<'tcx>, Option<GFnContract<ty::Instance<'tcx>>>)>) {
+    ) -> (GotocCtx<'tcx>, Vec<(MonoItem<'tcx>, Option<MonoContract<'tcx>>)>) {
         let items_with_contracts = with_timer(
             || collect_reachable_items(tcx, starting_items),
             "codegen reachability analysis",
@@ -282,7 +284,7 @@ impl CodegenBackend for GotocCodegenBackend {
                 let items = items_with_contracts
                     .into_iter()
                     .map(|(i, contract)| {
-                        if let Some(_) = contract {
+                        if contract.is_some() {
                             let instance = match i {
                                 MonoItem::Fn(f) => f,
                                 _ => unreachable!(),

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
@@ -176,7 +176,7 @@ pub fn extract_contract(tcx: TyCtxt, local_def_id: LocalDefId) -> super::contrac
 
         match hir_map.get_parent(hir_id) {
             Node::Item(Item { kind, .. }) => match kind {
-                ItemKind::Mod(m) => find_in_mod(*m),
+                ItemKind::Mod(m) => find_in_mod(m),
                 ItemKind::Impl(imp) => {
                     imp.items.iter().find(|it| it.ident.name == name).unwrap().id.hir_id()
                 }

diff --git a/kani-compiler/src/kani_middle/contracts.rs b/kani-compiler/src/kani_middle/contracts.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Basic type definitions for function contracts.
 use rustc_hir::def_id::DefId;
 
 /// Generic representation for a function contract. This is so that we can reuse

diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
@@ -15,6 +15,8 @@
 //! We have kept this module agnostic of any Kani code in case we can contribute this back to rustc.
 use tracing::{debug, debug_span, trace, warn};
 
+use std::collections::hash_map::Entry;
+
 use rustc_data_structures::fingerprint::Fingerprint;
 use rustc_data_structures::fx::{FxHashMap, FxHashSet};
 use rustc_data_structures::stable_hasher::{HashStable, StableHasher};
@@ -175,7 +177,7 @@ impl<'tcx> MonoItemsCollector<'tcx> {
     /// instruction looking for the items that should be included in the compilation.
     fn reachable_items(&mut self) {
         while let Some(to_visit) = self.queue.pop() {
-            if !self.collected.contains_key(&to_visit) {
+            if let Entry::Vacant(e) = self.collected.entry(to_visit) {
                 let opt_contract = to_visit.def_id().as_local().and_then(|local_def_id| {
                     let substs = match to_visit {
                         MonoItem::Fn(inst) => inst.substs,
@@ -200,7 +202,7 @@ impl<'tcx> MonoItemsCollector<'tcx> {
                 } else {
                     vec![]
                 };
-                self.collected.insert(to_visit, opt_contract);
+                e.insert(opt_contract);
                 let next_items = match to_visit {
                     MonoItem::Fn(instance) => self.visit_fn(instance),
                     MonoItem::Static(def_id) => self.visit_static(def_id),