Trait LlbcPass 

pub trait LlbcPass: Sync {
    // Provided methods
    fn should_run(&self, _options: &TranslateOptions) -> bool { ... }
    fn transform_body(&self, _ctx: &mut TransformCtx, _body: &mut ExprBody) { ... }
    fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) { ... }
    fn name(&self) -> &str { ... }
}

A pass that modifies llbc bodies.

Provided Methods

fn should_run(&self, _options: &TranslateOptions) -> bool

Whether the pass should run.

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 name(&self) -> &str

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

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors

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

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