CBMC symex fails on a function item called through `Box<dyn Fn>`: l2_rename_rvalues case address_of not handled

[srivatsansamraj]

I tried this code:

fn hook(x: &i32) {
    assert!(*x == 2);
}

#[kani::proof]
fn main() {
    let b: Box<dyn Fn(&i32)> = Box::new(hook);
    b(&2);
}

using the following command line invocation:

kani boxed_fn_item.rs

with Kani version: 0.68.0 with #4801 applied. Without it, codegen aborts first (#4800).

I expected to see this happen: verification succeeds. It does when hook is a closure instead of a function item.

Instead, this happened: codegen succeeds, but CBMC stops during symbolic execution with l2_rename_rvalues case `address_of' not handled.

@feliperodri reproduced the same failure with Box<Box<dyn Fn(&i32)>> over a function item, in review of #4801. He also pointed to #1257, where the same CBMC function fails on a struct expression.

The regression test from #4801, tests/kani/DynTrait/boxed_fn_item.rs, runs with --only-codegen because of this. It can move to full verification once this is fixed.