Field of type `Code` in struct when making closure

[danielsn]

When running the tests/kani/Refs/main.rs regression, we get the following error if we turn on typechecking for data-fields.

thread 'rustc' panicked at 'Illegal field.
        Name: 0
        Type: Code { parameters: [Parameter { typ: CInteger(SizeT), identifier: None, base_name: None }, Parameter { typ: CInteger(SizeT), identifier: None, base_name: None }], return_type: StructTag("tag-_12144896164184170153") }', /Users/dsn/ws/rmc/cprover_bindings/src/goto_program/typ.rs:187:9
stack backtrace:
   0: _rust_begin_unwind
   1: core::panicking::panic_fmt
   2: cprover_bindings::goto_program::typ::DatatypeComponent::field
             at /Users/dsn/ws/rmc/cprover_bindings/src/goto_program/typ.rs:187:9
   3: kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_struct_fields
             at /Users/dsn/ws/rmc/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:732:39
   4: kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_ty_tuple_like
             at /Users/dsn/ws/rmc/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:765:9
   5: kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_ty_closure::{{closure}}

Looks like we're codegenning Code instead of Code* when doing a closure

[tautschnig]

I believe we had actually seen this before: diffblue/cbmc#6370

[fzaiser]

Reduced test case:

#[kani::proof]
fn main() {
    f(h)
}

fn f(g: impl Fn() -> ()) {
    move || g();
}

fn h() {}

[fzaiser]

So I believe that the problem is that the move || g() closure stores the field g of type impl Fn() -> (). This gets compiled to Code { ... } (i.e. a C function type), but it should be compiled to a function pointer type. To fix this, we probably have to make sure that closures fields only store function pointers in GotoC, even if it is a move closure in Rust, i.e. if the field is not behind a reference in Rust.