Module driver 

Run the rustc compiler with our custom options and hooks.

Structs

CharonCallbacks

The callbacks for Charon

RunCompilerNormallyCallbacks

Dummy callbacks used to run the compiler normally when we shouldn’t be analyzing the crate.

Statics

SKIP_BORROWCK 🔒

Functions

def_id_debug 🔒

Custom DefId debug routine that doesn’t print unstable values like ids and hashes.

run_compiler_with_callbacks 🔒

Helper that runs the compiler and catches its fatal errors.

run_rustc_driver

Run the rustc driver with our custom hooks. Returns None if the crate was not compiled with charon (e.g. because it was a dependency). Otherwise returns the translated crate, ready for post-processing transformations.

set_mir_options 🔒

Tweak options to get usable MIR even for foreign crates.

set_no_codegen 🔒

Don’t even try to codegen. This avoids errors due to checking if the output filename is available (despite the fact that we won’t emit it because we stop compilation early).

set_skip_borrowck 🔒

setup_compiler 🔒

skip_borrowck_if_set 🔒