Current limitations of Charon

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.

Planned breaking changes

#287
#194
#582
Some potential rework of how we handle builtins like SliceIndexMut
Name matcher behavior likely to change in subtle ways (#319).

Known unsoundnesses

#583
#584

Unsupported Rust features

Tracked here: #142

Missing information in the translated output

Bodies of functions in foreign crates often cause errors (#543);
Bodies of std functions (#545);
Drops (#152);
Layout information (#581);
Lifetime information inside function bodies (not planned).