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,
    pub trusted_default: bool,
    pub ignore_default: 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.

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.