Crate charon_lib

Help

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§

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§

ast
common
errors: Utilities to generate error reports about the external dependencies.
export
ids
logger
name_matcher
options: The options that control charon behavior.
pretty: This module contains functions to pretty-print charon types.
transform

Macros§

code_location: 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
error: A custom log error macro. Uses the log crate.
error_assert: Custom assert to either panic or return an error
generate_index_type: 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.
info: A custom log info macro. Uses the log crate.
raise_error: Macro to either panic or return on error, depending on the CLI options
register_error
sanity_check: Custom assert to report an error and optionally panic
trace: A custom log trace macro. Uses the log crate.
warn: A custom log warn macro. Uses the log crate.

Constants§

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

Functions§