Struct move_stackless_bytecode::options::ProverOptions

pub struct ProverOptions {

    pub generate_only: bool,
    pub native_stubs: bool,
    pub minimize_execution_trace: bool,
    pub omit_model_debug: bool,
    pub stable_test_output: bool,
    pub verify_scope: VerificationScope,
    pub resource_wellformed_axiom: bool,
    pub assume_wellformed_on_access: bool,
    pub mutation: bool,
    pub mutation_add_sub: usize,
    pub mutation_sub_add: usize,
    pub mutation_mul_div: usize,
    pub mutation_div_mul: usize,
    pub boogie_poly: bool,
    pub deep_pack_unpack: bool,
    pub auto_trace_level: AutoTraceLevel,
    pub report_severity: Severity,
    pub dump_bytecode: bool,
    pub dump_cfg: bool,
    pub num_instances: usize,
    pub sequential_task: bool,
    pub check_inconsistency: bool,
    pub unconditional_abort_as_inconsistency: bool,
    pub for_interpretation: bool,
}

Fields

generate_only: bool

Whether to only generate backend code.

native_stubs: bool

Whether to generate stubs for native functions.

minimize_execution_trace: bool

Whether to minimize execution traces in errors.

omit_model_debug: bool

Whether to omit debug information in generated model.

stable_test_output: bool

Whether output for e.g. diagnosis shall be stable/redacted so it can be used in test output.

verify_scope: VerificationScope

Scope of what functions to verify.

resource_wellformed_axiom: bool

[deprecated] Whether to emit global axiom that resources are well-formed.

assume_wellformed_on_access: bool

Whether to assume wellformedness when elements are read from memory, instead of on function entry.

mutation: bool

Indicates that we should do any mutations

mutation_add_sub: usize

Indicates that we should use the add-subtract mutation on the given block

mutation_sub_add: usize

Indicates that we should use the subtract-add mutation on the given block

mutation_mul_div: usize

Indicates that we should use the multiply-divide mutation on the given block

mutation_div_mul: usize

Indicates that we should use the divide-multiply mutation on the given block

boogie_poly: bool

Whether to use the polymorphic boogie backend.

deep_pack_unpack: bool

Whether pack/unpack should recurse over the structure.

auto_trace_level: AutoTraceLevel

Auto trace level.

report_severity: Severity

Minimal severity level for diagnostics to be reported.

dump_bytecode: bool

Whether to dump the transformed stackless bytecode to a file

dump_cfg: bool

Whether to dump the control-flow graphs (in dot format) to files, one per each function

num_instances: usize

Number of Boogie instances to be run concurrently.

sequential_task: bool

Whether to run Boogie instances sequentially.

check_inconsistency: bool

Whether to check the inconsistency

unconditional_abort_as_inconsistency: bool

Whether to consider a function that abort unconditionally as an inconsistency violation

for_interpretation: bool

Whether to run the transformation passes for concrete interpretation (instead of proving)

Implementations

impl ProverOptions

pub fn get(env: &GlobalEnv) -> Rc<ProverOptions>

pub fn set(env: &GlobalEnv, options: ProverOptions)

Trait Implementations

impl Clone for ProverOptions

fn clone(&self) -> ProverOptions

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for ProverOptions

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

Formats the value using the given formatter.

impl Default for ProverOptions

fn default() -> Self

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for ProverOptions where
    ProverOptions: 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 ProverOptions

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

Serialize this value into the given Serde serializer.