pub struct FluxMetadata {Show 15 fields
pub enabled: bool,
pub cache: Option<bool>,
pub solver: Option<SmtSolver>,
pub scrape_quals: Option<bool>,
pub check_overflow: Option<OverflowMode>,
pub allow_uninterpreted_cast: Option<bool>,
pub smt_define_fun: Option<bool>,
pub default_trusted: Option<bool>,
pub default_ignore: Option<bool>,
pub include: Option<Vec<String>>,
pub include_trusted: Option<Vec<String>>,
pub include_trusted_impl: Option<Vec<String>>,
pub no_panic: Option<bool>,
pub lean: Option<LeanMode>,
pub dump_constraint: Option<bool>,
}Fields§
§enabled: bool§cache: Option<bool>Enables fixpoint query caching. Saves cache in target/FLUXCACHE
solver: Option<SmtSolver>Set the default solver
scrape_quals: Option<bool>Enable qualifier scrapping in fixpoint
check_overflow: Option<OverflowMode>Enable overflow checking
allow_uninterpreted_cast: Option<bool>Enable uninterpreted casts
smt_define_fun: Option<bool>Enable flux-defs to be defined as SMT functions
default_trusted: Option<bool>Set trusted to trusted
default_ignore: Option<bool>Set trusted to ignore
include: Option<Vec<String>>If present, only check files that match any of the glob patterns. Patterns are checked relative to the location of the manifest file.
include_trusted: Option<Vec<String>>If present, only consider DefId in files that match any of the glob patterns as trusted.
Patterns are checked relative to the location of the manifest file.
include_trusted_impl: Option<Vec<String>>If present, only consider DefId in files that match any of the glob patterns as trusted_impl.
Patterns are checked relative to the location of the manifest file.
no_panic: Option<bool>If present, every function in the module is implicitly labeled with a no_panic by default.
This means that the only way a function can panic is if it calls an external function without this attribute.
lean: Option<LeanMode>If present, enables lean mode
dump_constraint: Option<bool>If present, dumps the fixpoint constraint to a file