Struct CliOpts 

pub struct CliOpts {

    pub ullbc: bool,
    pub precise_drops: bool,
    pub skip_borrowck: bool,
    pub mir: Option<MirLevel>,
    pub rustc_args: Vec<String>,
    pub monomorphize: bool,
    pub monomorphize_mut: Option<MonomorphizeMut>,
    pub start_from: Vec<String>,
    pub include: Vec<String>,
    pub opaque: Vec<String>,
    pub exclude: Vec<String>,
    pub extract_opaque_bodies: bool,
    pub translate_all_methods: bool,
    pub remove_associated_types: Vec<String>,
    pub hide_marker_traits: bool,
    pub remove_adt_clauses: bool,
    pub hide_allocator: bool,
    pub remove_unused_self_clauses: bool,
    pub desugar_drops: bool,
    pub ops_to_function_calls: bool,
    pub index_to_function_calls: 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 no_erase_body_regions: bool,
    pub print_original_ullbc: bool,
    pub print_ullbc: bool,
    pub print_built_llbc: bool,
    pub print_llbc: bool,
    pub dest_dir: Option<PathBuf>,
    pub dest_file: Option<PathBuf>,
    pub no_dedup_serialized_ast: bool,
    pub no_serialize: bool,
    pub abort_on_error: bool,
    pub error_on_warnings: bool,
    pub preset: Option<Preset>,
}

Fields

ullbc: bool

Extract the unstructured LLBC (i.e., don’t reconstruct the control-flow)

precise_drops: bool

Whether to precisely translate drops and drop-related code. For this, we add explicit Destruct bounds to all generic parameters, set the MIR level to at least elaborated, and attempt to retrieve drop glue for all types.

This option is known to cause panics inside rustc, because their drop handling is not design to work on polymorphic types. To silence the warning, pass appropriate --opaque '{impl core::marker::Destruct for some::Type}' options.

Without this option, drops may be “conditional” and we may lack information about what code is run on drop in a given polymorphic function body.

skip_borrowck: bool

If activated, this skips borrow-checking of the crate.

mir: Option<MirLevel>

The MIR stage to extract. This is only relevant for the current crate; for dpendencies only MIR optimized is available.

rustc_args: Vec<String>

Extra flags to pass to rustc.

monomorphize: bool

Monomorphize the items encountered when possible. Generic items found in the crate are skipped. To only translate a particular call graph, use --start-from. Note: this doesn’t currently support dyn Trait.

monomorphize_mut: Option<MonomorphizeMut>

Partially monomorphize items to make it so that no item is ever monomorphized with a mutable reference (or type containing one); said differently, so that the presence of mutable references in a type is independent of its generics. This is used by Aeneas.

start_from: Vec<String>

A list of item paths to use as starting points for the translation. We will translate these items and any items they refer to, according to the opacity rules. When absent, we start from the path crate (which translates the whole crate).

include: Vec<String>

Whitelist of items to translate. These use the name-matcher syntax.

opaque: Vec<String>

Blacklist of items to keep opaque. Works just like --include, see the doc there.

exclude: Vec<String>

Blacklist of items to not translate at all. Works just like --include, see the doc there.

extract_opaque_bodies: bool

Usually we skip the bodies of foreign methods and structs with private fields. When this flag is on, we don’t.

translate_all_methods: bool

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

remove_associated_types: Vec<String>

Transforma the associate types of traits to be type parameters instead. This takes a list of name patterns of the traits to transform, using the same syntax as --include.

hide_marker_traits: bool

Whether to hide various marker traits such as Sized, Sync, Send and Destruct anywhere they show up. This can considerably speed up translation.

remove_adt_clauses: bool

Remove trait clauses from type declarations. Must be combined with --remove-associated-types for type declarations that use trait associated types in their fields, otherwise this will result in errors.

hide_allocator: bool

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

remove_unused_self_clauses: bool

Trait method declarations take a Self: Trait clause as parameter, so that they can be reused by multiple trait impls. This however causes trait definitions to be mutually recursive with their method declarations. This flag removes Self clauses that aren’t used to break this mutual recursion when possible.

desugar_drops: bool

Transform precise drops to the equivalent drop_in_place(&raw mut p) call.

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. Note that this may introduce UB since it creates references that were not normally created, including when indexing behind a raw pointer.

treat_box_as_builtin: bool

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

raw_consts: bool

Do not 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

Use DeBruijnVar::Free for the variables bound in item signatures, instead of DeBruijnVar::Bound everywhere. This simplifies the management of generics for projects that don’t intend to manipulate them too much.

no_erase_body_regions: bool

Disable the aeneas-only erasure of Body regions. Temporary flag to help migration.

print_original_ullbc: bool

Pretty-print the ULLBC immediately after extraction from MIR.

print_ullbc: bool

Pretty-print the ULLBC after applying the micro-passes (before serialization/control-flow reconstruction).

print_built_llbc: bool

Pretty-print the LLBC just after we built it (i.e., immediately after loop reconstruction).

print_llbc: bool

Pretty-print the final LLBC (after all the cleaning micro-passes).

dest_dir: Option<PathBuf>

The destination directory. Files will be generated as <dest_dir>/<crate_name>.{u}llbc, unless dest_file is set. dest_dir defaults to the current directory.

dest_file: Option<PathBuf>

The destination file. By default <dest_dir>/<crate_name>.llbc. If this is set we ignore dest_dir.

no_dedup_serialized_ast: bool

Don’t deduplicate values (types, trait refs) in the .(u)llbc file. This makes the file easier to inspect.

no_serialize: bool

Don’t serialize the final (U)LLBC to a file.

abort_on_error: bool

Panic on the first error. This is useful for debugging.

error_on_warnings: bool

Consider any warnings to be errors.

preset: Option<Preset>

Named builtin sets of options.

Implementations

impl CliOpts

pub fn apply_preset(&mut self)

pub fn validate(&self) -> Result<()>

Check that the options are meaningful

Trait Implementations

impl Args for CliOpts

fn group_id() -> Option<Id>

Report the [ArgGroup::id][crate::ArgGroup::id] for this set of arguments

fn augment_args<'b>(__clap_app: Command) -> Command

Append to [Command] so it can instantiate Self via [FromArgMatches::from_arg_matches_mut]

fn augment_args_for_update<'b>(__clap_app: Command) -> Command

Append to [Command] so it can instantiate self via [FromArgMatches::update_from_arg_matches_mut]

impl Clone for CliOpts

fn clone(&self) -> CliOpts

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for CliOpts

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for CliOpts

fn default() -> CliOpts

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for CliOpts

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl FromArgMatches for CliOpts

fn from_arg_matches(__clap_arg_matches: &ArgMatches) -> Result<Self, Error>

Instantiate Self from [ArgMatches], parsing the arguments as needed.

fn from_arg_matches_mut( __clap_arg_matches: &mut ArgMatches, ) -> Result<Self, Error>

Instantiate Self from [ArgMatches], parsing the arguments as needed.

fn update_from_arg_matches( &mut self, __clap_arg_matches: &ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

fn update_from_arg_matches_mut( &mut self, __clap_arg_matches: &mut ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

impl PartialEq for CliOpts

fn eq(&self, other: &CliOpts) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for CliOpts

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for CliOpts

impl StructuralPartialEq for CliOpts