Skip to content

Instantly share code, notes, and snippets.

@seyyedaliayati
Last active February 21, 2023 15:45
Show Gist options
  • Save seyyedaliayati/f8347501a39f660edc85232f0a11a060 to your computer and use it in GitHub Desktop.
Save seyyedaliayati/f8347501a39f660edc85232f0a11a060 to your computer and use it in GitHub Desktop.
pub struct ProverOptions {
/// Whether to only generate backend code.
pub generate_only: bool,
/// Whether to generate stubs for native functions.
pub native_stubs: bool,
/// Whether to minimize execution traces in errors.
pub minimize_execution_trace: bool,
/// Whether to omit debug information in generated model.
pub omit_model_debug: bool,
/// Whether output for e.g. diagnosis shall be stable/redacted so it can be used in test
/// output.
pub stable_test_output: bool,
/// Scope of what functions to verify.
pub verify_scope: VerificationScope,
/// [deprecated] Whether to emit global axiom that resources are well-formed.
pub resource_wellformed_axiom: bool,
/// Whether to assume wellformedness when elements are read from memory, instead of on
/// function entry.
pub assume_wellformed_on_access: bool,
/// Indicates that we should do any mutations
pub mutation: bool,
/// Indicates that we should use the add-subtract mutation on the given block
pub mutation_add_sub: usize,
/// Indicates that we should use the subtract-add mutation on the given block
pub mutation_sub_add: usize,
/// Indicates that we should use the multiply-divide mutation on the given block
pub mutation_mul_div: usize,
/// Indicates that we should use the divide-multiply mutation on the given block
pub mutation_div_mul: usize,
/// Whether to use the polymorphic boogie backend.
pub boogie_poly: bool,
/// Whether pack/unpack should recurse over the structure.
pub deep_pack_unpack: bool,
/// Auto trace level.
pub auto_trace_level: AutoTraceLevel,
/// Minimal severity level for diagnostics to be reported.
pub report_severity: Severity,
/// Whether to dump the transformed stackless bytecode to a file
pub dump_bytecode: bool,
/// Whether to dump the control-flow graphs (in dot format) to files, one per each function
pub dump_cfg: bool,
/// Number of Boogie instances to be run concurrently.
pub num_instances: usize,
/// Whether to run Boogie instances sequentially.
pub sequential_task: bool,
/// Whether to check the inconsistency
pub check_inconsistency: bool,
/// Whether to consider a function that abort unconditionally as an inconsistency violation
pub unconditional_abort_as_inconsistency: bool,
/// Whether to run the transformation passes for concrete interpretation (instead of proving)
pub for_interpretation: bool,
/// Whether to skip loop analysis.
pub skip_loop_analysis: bool,
/// Optional names of native methods (qualified with module name, e.g., m::foo) implementing
/// mutable borrow semantics
pub borrow_natives: Vec<String>,
/// Whether to ban convertion from int to bv at the boogie backend
pub ban_int_2_bv: bool,
}
// Default values are:
impl Default for ProverOptions {
fn default() -> Self {
Self {
generate_only: false,
native_stubs: false,
minimize_execution_trace: true,
omit_model_debug: false,
stable_test_output: false,
verify_scope: VerificationScope::All,
resource_wellformed_axiom: false,
assume_wellformed_on_access: false,
mutation: false,
mutation_add_sub: 0,
mutation_sub_add: 0,
mutation_mul_div: 0,
mutation_div_mul: 0,
boogie_poly: false,
deep_pack_unpack: false,
auto_trace_level: AutoTraceLevel::Off,
report_severity: Severity::Warning,
dump_bytecode: false,
dump_cfg: false,
num_instances: 1,
sequential_task: false,
check_inconsistency: false,
unconditional_abort_as_inconsistency: false,
for_interpretation: false,
skip_loop_analysis: false,
borrow_natives: vec![],
ban_int_2_bv: false,
}
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment