Struct TranslateOptions

pub struct TranslateOptions {
    pub mir_level: MirLevel,
    pub translate_all_methods: bool,
    pub no_code_duplication: bool,
    pub hide_marker_traits: bool,
    pub no_merge_goto_chains: bool,
    pub print_built_llbc: bool,
    pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
    pub remove_associated_types: Vec<NamePattern>,
}

The options that control translation and transformation.

Fields

mir_level: MirLevel

The level at which to extract the MIR

translate_all_methods: bool

Usually we skip the provided methods that aren’t used. When this flag is on, we translate them all.

no_code_duplication: bool

Error out if some code ends up being duplicated by the control-flow reconstruction (note that because several patterns in a match may lead to the same branch, it is node always possible not to duplicate code).

hide_marker_traits: bool

Whether to hide the Sized, Sync, Send and Unpin marker traits anywhere they show up.

no_merge_goto_chains: bool

Do not merge the chains of gotos.

print_built_llbc: bool

Print the llbc just after control-flow reconstruction.

item_opacities: Vec<(NamePattern, ItemOpacity)>

List of patterns to assign a given opacity to. Same as the corresponding TranslateOptions field.

remove_associated_types: Vec<NamePattern>

List of traits for which we transform associated types to type parameters.

Implementations

impl TranslateOptions

pub fn new(error_ctx: &mut ErrorCtx, options: &CliOpts) -> Self

pub fn opacity_for_name( &self, krate: &TranslatedCrate, name: &Name, ) -> ItemOpacity

Find the opacity requested for the given name. This does not take into account #[charon::opaque] annotations, only cli parameters.