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
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ impl GotocCtx<'_> {
.args
.iter()
.enumerate()
.filter(|&(_, arg)| (arg.mode != PassMode::Ignore))
.filter(|&(_, arg)| arg.mode != PassMode::Ignore)
.map(|(idx, arg)| {
let arg_name = format!("{fn_name}::param_{idx}");
let base_name = format!("param_{idx}");
Expand Down
8 changes: 8 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -204,6 +204,13 @@ impl<'tcx> GotocCtx<'tcx> {
Some(self.codegen_const_ptr(alloc, ty, inner_ty, loc))
}
TyKind::RigidTy(RigidTy::Adt(adt, args)) if adt.kind().is_struct() => {
//Special struct that is used to handle type_id function
if adt.name().contains("any::TypeId") {
let val = alloc.read_uint().unwrap();
let u128_expr = Expr::int_constant(val, Type::unsigned_int(128));
let typ = self.codegen_ty_stable(ty);
return Some(u128_expr.transmute_to(typ, &self.symbol_table));
}
// Structs only have one variant.
let variant = adt.variants_iter().next().unwrap();
// There must be at least one field associated with the scalar data.
Expand Down Expand Up @@ -399,6 +406,7 @@ impl<'tcx> GotocCtx<'tcx> {
let name = format!("{}::{alloc_id:?}", self.full_crate_name());
self.codegen_const_allocation(&alloc, Some(name), loc)
}
GlobalAlloc::TypeId { ty: _ } => todo!(),
};
assert!(res_t.is_pointer() || res_t.is_transparent_type(&self.symbol_table));
let offset_addr = base_addr
Expand Down
1 change: 1 addition & 0 deletions kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -529,6 +529,7 @@ fn collect_alloc_items(tcx: TyCtxt, alloc_id: AllocId) -> Vec<MonoItem> {
let vtable_id = vtable_alloc.vtable_allocation().unwrap();
items = collect_alloc_items(tcx, vtable_id);
}
GlobalAlloc::TypeId { ty: _ } => {}
};
items
}
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-2025-07-10"
channel = "nightly-2025-07-11"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
Loading