Struct bytecode::options::ProverOptions
source · pub struct ProverOptions {Show 24 fields
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§
source§impl ProverOptions
impl ProverOptions
pub fn get(env: &GlobalEnv) -> Rc<ProverOptions>
pub fn set(env: &GlobalEnv, options: ProverOptions)
Trait Implementations§
source§impl Clone for ProverOptions
impl Clone for ProverOptions
source§fn clone(&self) -> ProverOptions
fn clone(&self) -> ProverOptions
1.0.0 · source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source
. Read more