Struct Flags 

pub struct Flags {

    pub log_dir: PathBuf,
    pub include: Option<IncludePattern>,
    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 allow_uninterpreted_cast: bool,
    pub smt_define_fun: bool,
    pub check_overflow: OverflowMode,
    pub dump_constraint: bool,
    pub dump_checker_trace: Option<Level>,
    pub dump_fhir: bool,
    pub dump_rty: bool,
    pub dump_mir: bool,
    pub catch_bugs: bool,
    pub verify: bool,
    pub full_compilation: bool,
    pub trusted_default: bool,
    pub ignore_default: bool,
}

Fields

log_dir: PathBuf

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

include: Option<IncludePattern>

If present, only check files matching the IncludePattern a glob pattern.

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

allow_uninterpreted_cast: bool

Enables uninterpreted casts

smt_define_fun: bool

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

check_overflow: OverflowMode

If strict checks for over and underflow on arithmetic integer operations, If lazy checks for underflow and loses information if possible overflow, If none (default), it still checks for underflow on unsigned integer subtraction.

dump_constraint: bool

Dump constraints generated for each function (debugging)

dump_checker_trace: Option<Level>

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

Optimistically keeps running flux even after errors are found to get as many errors as possible

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.

trusted_default: bool

If true, all code is trusted by default. You can selectively untrust items by marking them with #[trusted(no)]. The default value of this flag is false, i.e., all code is untrusted by default.

ignore_default: bool

If true, all code will be ignored by default. You can selectively unignore items by marking them with #[ignore(no)]. The default value of this flag is false, i.e., all code is unignored by default.

Trait Implementations

impl Default for Flags

fn default() -> Self

Returns the “default value” for a type.