Crate charon_lib 

This library contains the definitions of the “LLBC” (Low-Level Borrow Calculus) AST, which faithfully captures the full and explicit contents of a Rust crate. The charon binary can translate any Rust crate to this AST, which can then be consumed for all sorts of purposes (most notably analysis, code generation, and execution).

The main type of this crate is ast::TranslatedCrate. To get one, call charon to get a serialized crate, then deserialize it using using deserialize_llbc. A crate is mainly composed of 5 kinds of items:

• Functions;
• Type definitions;
• Globals (constants and statics);
• Trait declarations;
• Trait implementations.

Each of these items is identified internally by a unique ast::ItemId, and externally by its ast::Name, such as “core::result::Result”. To find an item with a given name, have a look at the name matcher name_matcher::Patterns.

Function bodies come in two forms: “structured” or “unstructured”, depending on whether their control-flow is syntax-like (with blocks and scopes) or control-flow-like (with gotos). This can be chosen during translation. The corresponding ASTs can be found respectively in llbc_ast and ullbc_ast.

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;

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.

impl_from_enum

Implement From and TryFrom to wrap/unwrap enum variants with a single payload.

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

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

deserialize_llbc

Read a .llbc file.

deserialize_llbc_with_format

Read a serialized (U)LLBC file.