Trait LlbcPass 

pub trait LlbcPass: Sync {
    // Provided methods
    fn transform_body(&self, _ctx: &mut TransformCtx, _body: &mut ExprBody) { ... }
    fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) { ... }
    fn transform_ctx(&self, ctx: &mut TransformCtx) { ... }
    fn name(&self) -> &str { ... }
    fn log_before_body(&self, ctx: &TransformCtx, name: &Name, body: &Body) { ... }
}

A pass that modifies llbc bodies.

Provided Methods

fn transform_body(&self, _ctx: &mut TransformCtx, _body: &mut ExprBody)

Transform a body.

fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl)

Transform a function declaration. This forwards to transform_body by default.

fn transform_ctx(&self, ctx: &mut TransformCtx)

Transform the given context. This forwards to the other methods by default.

fn name(&self) -> &str

The name of the pass, used for debug logging. The default implementation uses the type name.

fn log_before_body(&self, ctx: &TransformCtx, name: &Name, body: &Body)

Log that the pass is about to be run on this body.

Implementors

impl LlbcPass for charon_lib::transform::control_flow::prettify_cfg::Transform

impl LlbcPass for charon_lib::transform::resugar::reconstruct_matches::Transform

impl LlbcPass for charon_lib::transform::simplify_output::index_to_function_calls::Transform

impl LlbcPass for charon_lib::transform::simplify_output::ops_to_function_calls::Transform