Trait UllbcPass

pub trait UllbcPass: Sync {
    // Provided methods
    fn transform_body(&self, _ctx: &mut TransformCtx<'_>, _body: &mut ExprBody) { ... }
    fn transform_function(
        &self,
        ctx: &mut TransformCtx<'_>,
        _decl: &mut FunDecl,
        body: Result<&mut ExprBody, Opaque>,
    ) { ... }
    fn transform_ctx(&self, ctx: &mut TransformCtx<'_>) { ... }
    fn name(&self) -> &str { ... }
    fn log_before_body(
        &self,
        ctx: &TransformCtx<'_>,
        name: &Name,
        body: Result<&ExprBody, &Opaque>,
    ) { ... }
}

A pass that modifies ullbc 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, body: Result<&mut ExprBody, Opaque>, )

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: Result<&ExprBody, &Opaque>, )

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

Implementors

impl UllbcPass for charon_lib::transform::merge_goto_chains::Transform

impl UllbcPass for charon_lib::transform::ops_to_function_calls::Transform

impl UllbcPass for charon_lib::transform::reconstruct_boxes::Transform

impl UllbcPass for charon_lib::transform::remove_arithmetic_overflow_checks::Transform

impl UllbcPass for charon_lib::transform::remove_dynamic_checks::Transform

impl UllbcPass for charon_lib::transform::simplify_constants::Transform

impl UllbcPass for charon_lib::transform::update_block_indices::Transform

impl UllbcPass for charon_lib::transform::update_closure_signatures::Transform