Struct Flags

pub struct Flags {

    pub log_dir: PathBuf,
    pub check_def: String,
    pub include: Option<GlobSet>,
    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: 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

include: Option<GlobSet>

If present, only check files matching a glob pattern. This flag can be specified multiple times and a file will be checked if it matches any of the patterns. Patterns are checked relative to the current working directory. For example, to check all the files in the ascii module of a crate, you can include the pattern "src/ascii/*" (assuming that’s where the files are located).

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: 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.