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 ops_to_function_calls: bool,
    pub index_to_function_calls: bool,
    pub print_built_llbc: bool,
    pub treat_box_as_builtin: bool,
    pub raw_consts: bool,
    pub reconstruct_fallible_operations: bool,
    pub reconstruct_asserts: bool,
    pub unbind_item_vars: bool,
    pub item_opacities: Vec<(NamePattern, ItemOpacity)>,
    pub remove_associated_types: Vec<NamePattern>,
    pub desugar_drops: bool,
    pub add_destruct_bounds: bool,
    pub translate_poly_drop_glue: bool,
    pub erase_body_lifetimes: bool,
}

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 various marker traits such as Sized, Sync, Send and Destruct 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.

ops_to_function_calls: bool

Transform array-to-slice unsizing, repeat expressions, and raw pointer construction into builtin functions in ULLBC.

index_to_function_calls: bool

Transform array/slice indexing into builtin functions in ULLBC.

print_built_llbc: bool

Print the llbc just after control-flow reconstruction.

treat_box_as_builtin: bool

Treat Box<T> as if it was a built-in type.

raw_consts: bool

Don’t inline or evaluate constants.

reconstruct_fallible_operations: bool

Replace “bound checks followed by UB-on-overflow operation” with the corresponding panic-on-overflow operation. This loses unwinding information.

reconstruct_asserts: bool

Replace “if x { panic() }” with “assert(x)”.

unbind_item_vars: bool

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.

desugar_drops: bool

Transform Drop to Call drop_in_place

add_destruct_bounds: bool

Add Destruct bounds to all generic params.

translate_poly_drop_glue: bool

Translate drop glue for poly types, knowing that this may cause ICEs.

erase_body_lifetimes: bool

Whether to erase all Body lifetimes at the end of translation.

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.