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
8 changes: 2 additions & 6 deletions cprover_bindings/src/goto_program/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -898,13 +898,9 @@ impl Type {
} else if concrete_self.is_scalar() && concrete_other.is_scalar() {
concrete_self == concrete_other
} else if concrete_self.is_struct_like() && concrete_other.is_scalar() {
concrete_self
.unwrap_transparent_type(st)
.map_or(false, |wrapped| wrapped == *concrete_other)
concrete_self.unwrap_transparent_type(st) == Some(concrete_other.clone())
} else if concrete_self.is_scalar() && concrete_other.is_struct_like() {
concrete_other
.unwrap_transparent_type(st)
.map_or(false, |wrapped| wrapped == *concrete_self)
concrete_other.unwrap_transparent_type(st) == Some(concrete_self.clone())
} else if concrete_self.is_struct_like() && concrete_other.is_struct_like() {
let self_components = concrete_self.get_non_empty_components(st).unwrap();
let other_components = concrete_other.get_non_empty_components(st).unwrap();
Expand Down
10 changes: 2 additions & 8 deletions cprover_bindings/src/irep/goto_binary_serde.rs
Original file line number Diff line number Diff line change
Expand Up @@ -704,10 +704,7 @@ where
/// Reads a reference encoded string from the byte stream.
fn read_numbered_string_ref(&mut self) -> io::Result<NumberedString> {
let string_number_result = self.read_usize_varenc();
let string_number = match string_number_result {
Ok(number) => number,
Err(error) => return Err(error),
};
let string_number = string_number_result?;
if self.is_first_read_string(string_number) {
// read raw string
let mut string_buf: Vec<u8> = Vec::new();
Expand Down Expand Up @@ -779,10 +776,7 @@ where
/// Reads a NumberedIrep from the byte stream.
fn read_numbered_irep_ref(&mut self) -> io::Result<NumberedIrep> {
let irep_number_result = self.read_usize_varenc();
let irep_number = match irep_number_result {
Ok(number) => number,
Err(error) => return Err(error),
};
let irep_number = irep_number_result?;

if self.is_first_read_irep(irep_number) {
let id = self.read_numbered_string_ref()?.number;
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1742,11 +1742,11 @@ impl<'tcx> GotocCtx<'tcx> {
/// TODO: Should we use `std_pointee_type` here?
/// <https://github.com/model-checking/kani/issues/1529>
pub fn is_fat_pointer(&self, pointer_ty: Ty<'tcx>) -> bool {
pointee_type(pointer_ty).map_or(false, |pointee_ty| self.use_fat_pointer(pointee_ty))
pointee_type(pointer_ty).is_some_and(|pointee_ty| self.use_fat_pointer(pointee_ty))
}

/// Check if the mir type already is a vtable fat pointer.
pub fn is_vtable_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool {
pointee_type(mir_type).map_or(false, |pointee_ty| self.use_vtable_fat_pointer(pointee_ty))
pointee_type(mir_type).is_some_and(|pointee_ty| self.use_vtable_fat_pointer(pointee_ty))
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -561,7 +561,7 @@ pub struct LoopInvariantRegister;
impl GotocHook for LoopInvariantRegister {
fn hook_applies(&self, _tcx: TyCtxt, instance: Instance) -> bool {
attributes::fn_marker(instance.def)
.map_or(false, |marker| marker == "kani_register_loop_contract")
.is_some_and(|marker| marker == "kani_register_loop_contract")
}

fn handle(
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/kani_middle/abi.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,18 +30,18 @@ impl LayoutOf {
/// This will also return `true` if the type is foreign.
pub fn has_foreign_tail(&self) -> bool {
self.unsized_tail()
.map_or(false, |t| matches!(t.kind(), TyKind::RigidTy(RigidTy::Foreign(_))))
.is_some_and(|t| matches!(t.kind(), TyKind::RigidTy(RigidTy::Foreign(_))))
}

/// Return whether the type is unsized and its tail is a trait object.
pub fn has_trait_tail(&self) -> bool {
self.unsized_tail().map_or(false, |t| t.kind().is_trait())
self.unsized_tail().is_some_and(|t| t.kind().is_trait())
}

/// Return whether the type is unsized and its tail is a slice.
#[allow(dead_code)]
pub fn has_slice_tail(&self) -> bool {
self.unsized_tail().map_or(false, |tail| {
self.unsized_tail().is_some_and(|tail| {
let kind = tail.kind();
kind.is_slice() | kind.is_str()
})
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/resolve/type_resolution.rs
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,7 @@ pub(super) fn is_type_primitive(typ: &syn::Type) -> bool {
}
Type::Path(TypePath { qself: None, path }) => path
.get_ident()
.map_or(false, |ident| PrimitiveIdent::from_str(&ident.to_string()).is_ok()),
.is_some_and(|ident| PrimitiveIdent::from_str(&ident.to_string()).is_ok()),
Type::BareFn(_)
| Type::Group(_)
| Type::ImplTrait(_)
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2024-11-15"
channel = "nightly-2024-11-16"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
Loading