Struct move_prover::cli::Options

pub struct Options {

    pub output_path: String,
    pub verbosity_level: LevelFilter,
    pub run_docgen: bool,
    pub run_abigen: bool,
    pub run_errmapgen: bool,
    pub run_read_write_set: bool,
    pub move_sources: Vec<String>,
    pub move_deps: Vec<String>,
    pub move_named_address_values: Vec<String>,
    pub experimental_pipeline: bool,
    pub model_builder: ModelBuilderOptions,
    pub docgen: DocgenOptions,
    pub prover: ProverOptions,
    pub backend: BoogieOptions,
    pub abigen: AbigenOptions,
    pub errmapgen: ErrmapOptions,
}

Represents options provided to the tool. Most of those options are configured via a toml source; some over the command line flags.

NOTE: any fields carrying structured data must appear at the end for making toml printing work. When changing this config, use mvp --print-config to verify this works.

Fields

output_path: String

The path to the boogie output which represents the verification problem.

verbosity_level: LevelFilter

Verbosity level for logging.

run_docgen: bool

Whether to run the documentation generator instead of the prover.

run_abigen: bool

Whether to run the ABI generator instead of the prover.

run_errmapgen: bool

Whether to run the error map generator instead of the prover.

run_read_write_set: bool

Whether to run the read write set analysis instead of the prover

move_sources: Vec<String>

The paths to the Move sources.

move_deps: Vec<String>

The paths to any dependencies for the Move sources. Those will not be verified but can be used by move_sources.

move_named_address_values: Vec<String>

The values assigned to named addresses in the Move code being verified.

experimental_pipeline: bool

Whether to run experimental pipeline

model_builder: ModelBuilderOptions

BEGIN OF STRUCTURED OPTIONS Options for the model builder.

docgen: DocgenOptions

Options for the documentation generator.

prover: ProverOptions

Options for the prover.

backend: BoogieOptions

Options for the prover backend.

abigen: AbigenOptions

Options for the ABI generator.

errmapgen: ErrmapOptions

Options for the error map generator. TODO: this currently create errors during deserialization, so skip them for this.

Implementations

impl Options

pub fn create_from_toml(toml_source: &str) -> Result<Options>

Creates options from toml configuration source.

pub fn create_from_toml_file(toml_file: &str) -> Result<Options>

Creates options from toml configuration file.

pub fn create_from_args(args: &[String]) -> Result<Options>

pub fn setup_logging(&self)

Sets up logging based on provided options. This should be called as early as possible and before any use of info!, warn! etc.

pub fn setup_logging_for_test(&self)

pub fn enable_debug(&mut self)

Convenience function to enable debugging (like high verbosity) on this instance.

Trait Implementations

impl Clone for Options

fn clone(&self) -> Options

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Options

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

Formats the value using the given formatter.

impl Default for Options

fn default() -> Self

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for Optionswhere Options: Default,

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Serialize for Options

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

Serialize this value into the given Serde serializer.