diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index a764132034e9..16afb80a1b5e 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -47,7 +47,7 @@ jobs: - name: 'Run Clippy' run: | - cargo clippy --workspace -- -D warnings + cargo clippy --workspace --tests -- -D warnings RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings - name: 'Print Clippy Statistics' diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index 5a0ad76b81c6..df1503b60201 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/cprover_bindings/src/goto_program/typ.rs @@ -1427,69 +1427,6 @@ impl Type { } types } - - /// Generate a string which uniquely identifies the given type - /// while also being a valid variable/funcion name - pub fn to_identifier(&self) -> String { - // Use String instead of InternedString, since we don't want to intern temporaries. - match self { - Type::Array { typ, size } => { - format!("array_of_{size}_{}", typ.to_identifier()) - } - Type::Bool => "bool".to_string(), - Type::CBitField { width, typ } => { - format!("cbitfield_of_{width}_{}", typ.to_identifier()) - } - Type::CInteger(int_kind) => format!("c_int_{int_kind:?}"), - // e.g. `int my_func(double x, float_y) {` - // => "code_from_double_float_to_int" - Type::Code { parameters, return_type } => { - let parameter_string = parameters - .iter() - .map(|param| param.typ().to_identifier()) - .collect::>() - .join("_"); - let return_string = return_type.to_identifier(); - format!("code_from_{parameter_string}_to_{return_string}") - } - Type::Constructor => "constructor".to_string(), - Type::Double => "double".to_string(), - Type::Empty => "empty".to_string(), - Type::FlexibleArray { typ } => format!("flexarray_of_{}", typ.to_identifier()), - Type::Float => "float".to_string(), - Type::Float16 => "float16".to_string(), - Type::Float128 => "float128".to_string(), - Type::IncompleteStruct { tag } => tag.to_string(), - Type::IncompleteUnion { tag } => tag.to_string(), - Type::InfiniteArray { typ } => { - format!("infinite_array_of_{}", typ.to_identifier()) - } - Type::Integer => "integer".to_string(), - Type::Pointer { typ } => format!("pointer_to_{}", typ.to_identifier()), - Type::Signedbv { width } => format!("signed_bv_{width}"), - Type::Struct { tag, .. } => format!("struct_{tag}"), - Type::StructTag(tag) => format!("struct_tag_{tag}"), - Type::TypeDef { name: tag, .. } => format!("type_def_{tag}"), - Type::Union { tag, .. } => format!("union_{tag}"), - Type::UnionTag(tag) => format!("union_tag_{tag}"), - Type::Unsignedbv { width } => format!("unsigned_bv_{width}"), - // e.g. `int my_func(double x, float_y, ..) {` - // => "variadic_code_from_double_float_to_int" - Type::VariadicCode { parameters, return_type } => { - let parameter_string = parameters - .iter() - .map(|param| param.typ().to_identifier()) - .collect::>() - .join("_"); - let return_string = return_type.to_identifier(); - format!("variadic_code_from_{parameter_string}_to_{return_string}") - } - Type::Vector { typ, size } => { - let typ = typ.to_identifier(); - format!("vec_of_{size}_{typ}") - } - } - } } #[cfg(test)] @@ -1509,14 +1446,6 @@ mod type_tests { assert_eq!(type_def.type_name().unwrap().to_string(), format!("tag-{NAME}")); } - #[test] - fn check_typedef_identifier() { - let type_def = Bool.to_typedef(NAME); - let id = type_def.to_identifier(); - assert!(id.ends_with(NAME)); - assert!(id.starts_with("type_def")); - } - #[test] fn check_typedef_create() { assert!(matches!(Bool.to_typedef(NAME), TypeDef { .. })); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 2392a801809f..b82a0c108424 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -101,7 +101,6 @@ pub enum PropertyClass { Unreachable, } -#[allow(dead_code)] impl PropertyClass { pub fn as_str(&self) -> &str { self.as_ref() diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 9b46eb2e7d09..060f68ac88f7 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -747,7 +747,7 @@ mod tests { fn length_one_item_prefix() { let generic_args = "::"; let name = "unchecked_add"; - let item_path = format!("NonZero{}::{}", generic_args, name); + let item_path = format!("NonZero{generic_args}::{name}"); assert!(last_two_items_of_path_match(&item_path, generic_args, name)) } @@ -755,7 +755,7 @@ mod tests { fn length_three_item_prefix() { let generic_args = "::"; let name = "unchecked_add"; - let item_path = format!("core::num::NonZero{}::{}", generic_args, name); + let item_path = format!("core::num::NonZero{generic_args}::{name}"); assert!(last_two_items_of_path_match(&item_path, generic_args, name)) } diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 6f7b59041d12..60b99e5cf13d 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -2,6 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // //! Utility functions that allow us to modify a function body. +//! +//! TODO: We should not need this code anymore now that https://github.com/rust-lang/rust/pull/138536 is merged use crate::kani_middle::kani_functions::KaniHook; use crate::kani_queries::QueryDb; @@ -54,12 +56,10 @@ impl MutableBody { &self.locals } - #[allow(dead_code)] pub fn arg_count(&self) -> usize { self.arg_count } - #[allow(dead_code)] pub fn var_debug_info(&self) -> &Vec { &self.var_debug_info } @@ -328,7 +328,6 @@ impl MutableBody { /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the /// terminator of the newly inserted basic block. - #[allow(dead_code)] pub fn insert_bb( &mut self, mut bb: BasicBlock,