charon icon indicating copy to clipboard operation
charon copied to clipboard

Failure on function returning iterator with lifetime annotation

Open R1kM opened this issue 4 months ago • 0 comments

Charon commit https://github.com/AeneasVerif/charon/commit/e0b2b31542eaf8725757880ec62f27bc00a0007f aborts on the following code with error message Compilation failed: error: Unimplemented: Alias(Alias { kind: Opaque, args: [Lifetime(Region { kind: ReEarlyParam(EarlyParamRegion { index: 0, name: "'a" }) }), Lifetime(Region { kind: ReEarlyParam(EarlyParamRegion { index: 0, name: "'a" }) })], def_id: test_crate::sparse_transitions::{opaque#0} })

fn sparse_transitions<'a>() -> impl Iterator<Item = u8> + 'a {
    core::iter::from_fn(move || { None })
}

Note, while this specifc snppet mentions EarlyParamRegion, this does not seem due to a lack of support for them. Other code snippets also fail with args such as Lifetime(Region { kind: ReErased }

R1kM avatar Oct 01 '24 18:10 R1kM