Trait UllbcPass

Source

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) { ... }
    fn transform_ctx(&self, ctx: &mut TransformCtx) { ... }
    fn name(&self) -> &str { ... }
    fn log_before_body(
        &self,
        ctx: &TransformCtx,
        name: &Name,
        body: Result<&ExprBody, &Opaque>,
    ) { ... }
}

Expand description

A pass that modifies ullbc bodies.

Provided Methods§

Source

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

Transform a body.

Source

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

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

Source

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

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

Source

fn name(&self) -> &str

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

Source

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§

Source §

impl UllbcPass for charon_lib::transform::inline_local_panic_functions::Transform

Source §

impl UllbcPass for charon_lib::transform::inline_promoted_consts::Transform

Source §

impl UllbcPass for charon_lib::transform::insert_assign_return_unit::Transform

Source §

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

Source §

impl UllbcPass for charon_lib::transform::reconstruct_asserts::Transform

Source §

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

The special alloc::boxed::box_new(x) intrinsic becomes the following:

@2 := size_of<i32>
@3 := align_of<i32>
@4 := alloc::alloc::exchange_malloc(move (@2), move (@3))
storage_live(@5)
@5 := shallow_init_box::<i32>(move (@4))
// possibly some intermediate statements
*(@5) := x

We reconstruct this into a call to Box::new(x).

Source §