Proposed change: add a test that reaches GotocCtx::deref_box (kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs) and the is_box() branch of place codegen that calls it (codegen/place.rs), or remove both. They look unreachable on the current toolchain. rustc's ElaborateBoxDerefs pass rewrites *b on a Box into field projections through Unique and NonNull before Kani sees the body.
Motivation: @feliperodri tested this in review of #4801. He put a panic! at the top of deref_box, and the whole kani suite still passed, 611 of 611:
// kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs, first line of deref_box
panic!("deref_box reached");let x = *b; and (*boxed_dyn)(&2) both codegen without reaching it.
#4801 kept deref_box in step with box_value, because the two drifting apart caused #4800. But no test can show that half of the change working or breaking. If no MIR reaches the branch after elaboration, removing it leaves two readers of the chain: box_value and codegen_ptr_out_of_wrappers. I can take either option.
Proposed change: add a test that reaches
GotocCtx::deref_box(kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs) and theis_box()branch of place codegen that calls it (codegen/place.rs), or remove both. They look unreachable on the current toolchain. rustc'sElaborateBoxDerefspass rewrites*bon aBoxinto field projections throughUniqueandNonNullbefore Kani sees the body.Motivation: @feliperodri tested this in review of #4801. He put a
panic!at the top ofderef_box, and the wholekanisuite still passed, 611 of 611:let x = *b;and(*boxed_dyn)(&2)both codegen without reaching it.#4801 kept
deref_boxin step withbox_value, because the two drifting apart caused #4800. But no test can show that half of the change working or breaking. If no MIR reaches the branch after elaboration, removing it leaves two readers of the chain:box_valueandcodegen_ptr_out_of_wrappers. I can take either option.