Example: boxed closures, like this:

   // Create a boxed once-callable closure
    let f: Box<dyn FnOnce()> = Box::new(|| {});
    f();

We need to investigate these. Currently, kani print warnings like the one above for these issues:

WARN kani_compiler::codegen_cprover_gotoc::codegen::place Unexpected type mismatch in projection:
Expr { value: Member { lhs: Expr { value: Symbol { identifier: "_ZN4core3num7flt2dec17digits_to_dec_str17h455a99ccc8826c4bE::1::var_4::parts" }, typ: StructTag("tag-_15158566036879639663"), location: None }, field: "data" }, typ: Pointer { typ: UnionTag("tag-_7532365074337032130") }, location: None }
Expr type
Pointer { typ: UnionTag("tag-_7532365074337032130") }
Type from MIR
FlexibleArray { typ: UnionTag("tag-_7532365074337032130") }

Not that I have a solution here as to why "Pointer" and "FlexibleArray" seem to be confused here, but I just wanted to note that CBMC now takes a #flexible_array_member annotation on flexible array members.

From what I gather so far, it looks like we are incorrectly using Struct { Pointer } when adding the symbol to the symbol table. Trying to pin down where this is happening.

Oh, I think I found it. :)

It looks like we are assuming in a lot of places in this file that a slice is encoded as:

struct<T> Slice{
   data: const* T,
   len: usize,
}

But in the following line we expect a FlexibleArray: