Aymeric Fromherz

Mismatched GenericParams

2

When running Charon commit 65c45918 on the crate ordnung commit e1f1e3bd, the following error related to mismatched generics appears: ``` error: Mismatched generics: expected: GenericParams { regions: [], types: [Some(TypeVar...

Add support for virtual manifests

2

When running Charon on a virtual manifest, e.g., serde, Charon currently crashes with the following error message ``` error: manifest path `/Users/fromherz/Work/papers/charon-tool-paper/tools/serde/Cargo.toml` is a virtual manifest, but this command requires...

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" })...

Charon commit e0b2b31 aborts on the following code with error message `Compilation failed: error: Unexpected `ShallowInitBox`` ```rust use std::vec; pub struct Error { messages: Vec, } pub struct IntoIter {...

Normalization binder error

1

The following code ```rust pub struct S; impl S { pub fn f Option { None } } ``` crashes on Charon version 8fe7c7311 with the following error message ```...