We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent b4b6736 commit 75e754aCopy full SHA for 75e754a
src/kani-compiler/rustc_codegen_kani/src/codegen/operand.rs
@@ -392,7 +392,11 @@ impl<'tcx> GotocCtx<'tcx> {
392
base_addr
393
.cast_to(Type::unsigned_int(8).to_pointer())
394
.plus(Expr::int_constant(offset.bytes(), Type::unsigned_int(64)))
395
- .cast_to(res_t)
+ // The `cast_to` operation causes https://github.com/model-checking/kani/issues/822
396
+ // FIXME: Changing to a transmute to temporarily unblock, proper fix is to
397
+ // unwrap the transparent struct.
398
+ .transmute_to(res_t, &self.symbol_table)
399
+ //.cast_to(res_t)
400
}
401
402
pub fn codegen_allocation_auto_imm_name<F: FnOnce(&mut GotocCtx<'tcx>) -> String>(
tests/kani/Repr/check_repr_fixme.rs renamed to tests/kani/Repr/check-repr.rs
0 commit comments