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 GOTO
s).
Re-exports§
pub use ast::builtins;
pub use ast::expressions;
pub use ast::gast;
pub use ast::llbc_ast;
pub use ast::meta;
pub use ast::names;
pub use ast::types;
pub use ast::ullbc_ast;
pub use ast::values;
pub use pretty::formatter;
pub use transform::graphs;
pub use transform::reorder_decls;
pub use transform::ullbc_to_llbc;
Modules§
- Utilities to generate error reports about the external dependencies.
- The options received as input by cargo-charon
- This module contains functions to pretty-print charon types.
Macros§
- This macro computes the name of the function in which it is called and the line number. We adapted it from: https://stackoverflow.com/questions/38088067/equivalent-of-func-or-function-in-rust
- A custom log error macro. Uses the log crate.
- Custom assert to either panic or return an error
- Macro to either panic or return on error, depending on the CLI options
- Generate an
Index
index type. We use it because we need manipulate a lot of different indices (for various kinds of declarations, variables, blocks, etc.). For sanity, we prevent any confusion between the different kinds of indices by using different types. The following macro allows us to easily derive those types. - A custom log info macro. Uses the log crate.
- A custom log trace macro. Uses the log crate.
- A custom log warn macro. Uses the log crate.
Constants§
- VERSION 🔒The version of the crate, as defined in
Cargo.toml
.