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

source

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

source

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

Trait Implementations§

source§

impl Clone for ProverOptions

source§

fn clone(&self) -> ProverOptions

Returns a copy of the value. Read more
1.0.0 · source§

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

Performs copy-assignment from source. Read more
source§

impl Debug for ProverOptions

source§

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

Formats the value using the given formatter. Read more
source§

impl Default for ProverOptions

source§

fn default() -> Self

Returns the “default value” for a type. Read more
source§

impl<'de> Deserialize<'de> for ProverOptionswhere ProverOptions: Default,

source§

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

Deserialize this value from the given Serde deserializer. Read more
source§

impl Serialize for ProverOptions

source§

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

Serialize this value into the given Serde serializer. Read more

Auto Trait Implementations§

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

const: unstable · source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for Twhere T: ?Sized,

const: unstable · source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<T> From<T> for T

const: unstable · source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

impl<T, U> Into<U> for Twhere U: From<T>,

const: unstable · source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T> Same<T> for T

§

type Output = T

Should always be Self
source§

impl<T> ToOwned for Twhere T: Clone,

§

type Owned = T

The resulting type after obtaining ownership.
source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
source§

impl<T, U> TryFrom<U> for Twhere U: Into<T>,

§

type Error = Infallible

The type returned in the event of a conversion error.
const: unstable · source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for Twhere U: TryFrom<T>,

§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
const: unstable · source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<V, T> VZip<V> for Twhere V: MultiLane<T>,

§

fn vzip(self) -> V

source§

impl<T> DeserializeOwned for Twhere T: for<'de> Deserialize<'de>,