Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/format-check.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand Down
71 changes: 0 additions & 71 deletions cprover_bindings/src/goto_program/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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::<Vec<_>>()
.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::<Vec<_>>()
.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)]
Expand All @@ -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 { .. }));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,6 @@ pub enum PropertyClass {
Unreachable,
}

#[allow(dead_code)]
impl PropertyClass {
pub fn as_str(&self) -> &str {
self.as_ref()
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/resolve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -747,15 +747,15 @@ mod tests {
fn length_one_item_prefix() {
let generic_args = "::<u32>";
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))
}

#[test]
fn length_three_item_prefix() {
let generic_args = "::<u32>";
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))
}

Expand Down
5 changes: 2 additions & 3 deletions kani-compiler/src/kani_middle/transform/body.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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<VarDebugInfo> {
&self.var_debug_info
}
Expand Down Expand Up @@ -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,
Expand Down
Loading