Struct CharonCallbacks

pub struct CharonCallbacks<'a> {
    options: &'a CliOpts,
    transform_ctx: Option<TransformCtx>,
}

The callbacks for Charon

Fields

options: &'a CliOpts

transform_ctx: Option<TransformCtx>

This is to be filled during the extraction; it contains the translated crate.

Trait Implementations

impl<'a> Callbacks for CharonCallbacks<'a>

fn after_expansion<'tcx>( &mut self, compiler: &Compiler, tcx: TyCtxt<'tcx>, ) -> Compilation

The MIR is modified in place: borrow-checking requires the “promoted” MIR, which causes the “built” MIR (which results from the conversion to HIR to MIR) to become unaccessible. Because we require built MIR at the moment, we hook ourselves before MIR-based analysis passes.

fn config(&mut self, config: &mut Config)

Called before creating the compiler instance

fn after_analysis<'tcx>(&mut self, _: &Compiler, _: TyCtxt<'tcx>) -> Compilation

Called after analysis. Return value instructs the compiler whether to continue the compilation afterwards (defaults to Compilation::Continue)

fn after_crate_root_parsing( &mut self, _compiler: &Compiler, _krate: &mut Crate, ) -> Compilation

Called after parsing the crate root. Submodules are not yet parsed when this callback is called. Return value instructs the compiler whether to continue the compilation afterwards (defaults to Compilation::Continue)