Crate charon_lib

source
Expand description

This library contains utilities to extract the MIR from a Rust project, by compiling it to an easy-to-use AST called LLBC (Low-Level Borrow Calculus). This AST is serialized into JSON files.

A good entry point to explore the project is driver, and in particular driver::CharonCallbacks, which implements the callback which we provide to Rustc.

The ASTs are in ullbc_ast (Unstructured LLBC - basically a cleaned-up version of MIR) and llbc_ast (same as ULLBC, but we reconstructed the control-flow to have if ... then ... else ..., loops, etc. instead of GOTOs).

Re-exports§

Modules§

Macros§

Constants§

  • VERSION 🔒
    The version of the crate, as defined in Cargo.toml.