Struct boogie_backend::options::BoogieOptions

pub struct BoogieOptions {

    pub boogie_exe: String,
    pub use_exp_boogie: bool,
    pub z3_exe: String,
    pub use_cvc4: bool,
    pub cvc4_exe: String,
    pub debug_trace: bool,
    pub boogie_flags: Vec<String>,
    pub use_array_theory: bool,
    pub generate_smt: bool,
    pub native_equality: bool,
    pub type_requires: String,
    pub stratification_depth: usize,
    pub aggressive_func_inline: String,
    pub func_inline: String,
    pub serialize_bound: usize,
    pub bench_repeat: usize,
    pub vector_using_sequences: bool,
    pub random_seed: usize,
    pub proc_cores: usize,
    pub vc_timeout: usize,
    pub keep_artifacts: bool,
    pub eager_threshold: usize,
    pub lazy_threshold: usize,
    pub stable_test_output: bool,
    pub num_instances: usize,
    pub sequential_task: bool,
    pub hard_timeout_secs: u64,
    pub vector_theory: VectorTheory,
    pub z3_trace_file: Option<String>,
}

Boogie options.

Fields

boogie_exe: String

Path to the boogie executable.

use_exp_boogie: bool

Use experimental boogie exe found via env var EXP_BOOGIE_EXE.

z3_exe: String

Path to the z3 executable.

use_cvc4: bool

Whether to use cvc4.

cvc4_exe: String

Path to the cvc4 executable.

debug_trace: bool

Whether to generate debug trace code.

boogie_flags: Vec<String>

List of flags to pass on to boogie.

use_array_theory: bool

Whether to use native array theory.

generate_smt: bool

Whether to produce an SMT file for each verification problem.

native_equality: bool

Whether native instead of stratified equality should be used.

type_requires: String

A string determining the type of requires used for parameter type checks. Can be "requires" or "free requires“.

stratification_depth: usize

The depth until which stratified functions are expanded.

aggressive_func_inline: String

A string to be used to inline a function of medium size. Can be empty or {:inline}.

func_inline: String

A string to be used to inline a function of small size. Can be empty or {:inline}.

serialize_bound: usize

A bound to apply to the length of serialization results.

bench_repeat: usize

How many times to call the prover backend for the verification problem. This is used for benchmarking.

vector_using_sequences: bool

Whether to use the sequence theory as the internal representation for $Vector type.

random_seed: usize

A seed for the prover.

proc_cores: usize

The number of cores to use for parallel processing of verification conditions.

vc_timeout: usize

A (soft) timeout for the solver, per verification condition, in seconds.

keep_artifacts: bool

Whether Boogie output and log should be saved.

eager_threshold: usize

Eager threshold for quantifier instantiation.

lazy_threshold: usize

Lazy threshold for quantifier instantiation.

stable_test_output: bool

Whether to use the new Boogie {:debug ..} attribute for tracking debug values.

num_instances: usize

Number of Boogie instances to be run concurrently.

sequential_task: bool

Whether to run Boogie instances sequentially.

hard_timeout_secs: u64

A hard timeout for boogie execution; if the process does not terminate within this time frame, it will be killed. Zero for no timeout.

vector_theory: VectorTheory

What vector theory to use.

z3_trace_file: Option<String>

Whether to generate a z3 trace file and where to put it.

Implementations

impl BoogieOptions

pub fn derive_options(&mut self)

Derive options based on other set options.

pub fn get_boogie_command(&self, boogie_file: &str) -> Result<Vec<String>>

Returns command line to call boogie.

pub fn get_boogie_log_file(&self, boogie_file: &str) -> String

Returns name of file where to log boogie output.

pub fn adjust_timeout(&self, time: usize) -> usize

Adjust a timeout value, given in seconds, for the runtime environment.

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

Checks whether the expected tool versions are installed in the environment.

Trait Implementations

impl Clone for BoogieOptions

fn clone(&self) -> BoogieOptions

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for BoogieOptions

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

Formats the value using the given formatter.

impl Default for BoogieOptions

fn default() -> Self

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for BoogieOptionswhere BoogieOptions: 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 BoogieOptions

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

Serialize this value into the given Serde serializer.