Struct Flags

pub struct Flags {

    pub log_dir: PathBuf,
    pub check_def: String,
    pub check_files: Paths,
    pub pointer_width: PointerWidth,
    pub cache: Option<PathBuf>,
    pub verbose: bool,
    pub annots: bool,
    pub timings: bool,
    pub solver: SmtSolver,
    pub scrape_quals: bool,
    pub smt_define_fun: bool,
    pub check_overflow: bool,
    pub dump_constraint: bool,
    pub dump_checker_trace: bool,
    pub dump_fhir: bool,
    pub dump_rty: bool,
    pub dump_mir: bool,
    pub catch_bugs: bool,
    pub verify: bool,
    pub full_compilation: bool,
}

Fields

log_dir: PathBuf

Sets the directory to dump data. Defaults to ./log/.

check_def: String

Only checks definitions containing name as a substring

check_files: Paths

Only checks the specified files. Takes a list of comma separated paths

pointer_width: PointerWidth

Set the pointer size (either 32 or 64), used to determine if an integer cast is lossy (default 64).

cache: Option<PathBuf>

If present switches on query caching and saves the cache in the provided path

verbose: bool

annots: bool

Compute statistics about number and size of annotations. Dumps file to [Self.log_dir]

timings: bool

Print statistics about time taked to analyze each fuction. Also dumps a file with the raw times for each function.

solver: SmtSolver

Default solver. Either z3 or cvc5.

scrape_quals: bool

Enables qualifier scrapping in fixpoint

smt_define_fun: bool

Translates monomorphic defs functions into SMT define-fun instead of inlining them away inside flux.

check_overflow: bool

If true checks for over and underflow on arithmetic integer operations, default false. When set to false, it still checks for underflow on unsigned integer subtraction.

dump_constraint: bool

Dump constraints generated for each function (debugging)

dump_checker_trace: bool

Saves the checker’s trace (debugging)

dump_fhir: bool

Saves the fhir for each item (debugging)

dump_rty: bool

Saves the the fhir (debugging)

dump_mir: bool

Saves the low-level MIR for each analyzed function (debugging)

catch_bugs: bool

Saves the low-level MIR for each analyzed function (debugging)

verify: bool

Whether verification for the current crate is enabled. If false (the default), flux-driver will behave exactly like rustc. This flag is managed by the cargo flux and flux binaries, so you don’t need to mess with it.

full_compilation: bool

If true, produce artifacts after analysis. This flag is managed by cargo flux, so you don’t typically have to set it manually.

Trait Implementations

impl Default for Flags

fn default() -> Self

Returns the “default value” for a type.