Struct TranslateOptions

pub struct TranslateOptions {

    pub mir_level: MirLevel,
    pub translate_all_methods: bool,
    pub monomorphize_mut: Option<MonomorphizeMut>,
    pub hide_marker_traits: bool,
    pub remove_adt_clauses: bool,
    pub hide_allocator: bool,
    pub remove_unused_self_clauses: bool,
    pub monomorphize_with_hax: bool,
    pub no_ops_to_function_calls: bool,
    pub no_merge_goto_chains: bool,
    pub print_built_llbc: bool,
    pub raw_boxes: 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.

monomorphize_mut: Option<MonomorphizeMut>

If Some(_), run the partial mutability monomorphization pass. The contained enum indicates whether to partially monomorphize types.

hide_marker_traits: bool

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

remove_adt_clauses: bool

Remove trait clauses attached to type declarations.

hide_allocator: bool

Hide the A type parameter on standard library containers (Box, Vec, etc).

remove_unused_self_clauses: bool

Remove unused Self: Trait clauses on method declarations.

monomorphize_with_hax: bool

Monomorphize code using hax’s instantiation mechanism.

no_ops_to_function_calls: bool

Transforms ArrayToSlice, Repeat, and RawPtr aggregates to builtin function calls.

no_merge_goto_chains: bool

Do not merge the chains of gotos.

print_built_llbc: bool

Print the llbc just after control-flow reconstruction.

raw_boxes: bool

Don’t special-case the translation of Box<T>

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.