pub struct Flags {Show 22 fields
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 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
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.