Charon is alpha software. In particular, it is currently poorly documented, doesn't support all the Rust features we'd like, and has several breaking changes planned in the near future.
- AeneasVerif#287
- AeneasVerif#194
- AeneasVerif#582
- Some potential rework of how we handle builtins like
SliceIndexMut - Name matcher behavior likely to change in subtle ways (AeneasVerif#319).
Tracked here: AeneasVerif#142
- Bodies of functions in foreign crates often cause errors (AeneasVerif#543);
- Bodies of std functions (AeneasVerif#545);
- Drops (AeneasVerif#152);
- Layout information (AeneasVerif#581);
- Lifetime information inside function bodies (not planned).