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

check_late_rustc_errors 🔒

Run rustc checks that normally happen close to codegen, so that we get all the post-mono errors etc.

def_id_debug 🔒

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

precheck_rustc_errors 🔒

Run a couple of rustc queries that don’t involve MIR (so that they don’t steal it). Returns whether rustc reported errors. This lets us avoid running Charon translation on crates rustc already rejects.

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_parallel_frontend 🔒

Enable rustc’s parallel front-end.

set_skip_borrowck 🔒

setup_compiler 🔒

setup_miri_sysroot 🔒

cargo miri setup sets up a sysroot containing a standard library built with -Zalways-encode-mir.

skip_borrowck_if_set 🔒