flux_bin/
lib.rs

1use cargo_metadata::camino::Utf8Path;
2use flux_config::{LeanMode, OverflowMode, SmtSolver};
3use serde::Deserialize;
4
5pub mod cargo_flux_opts;
6pub mod cargo_style;
7pub mod utils;
8
9#[derive(Deserialize, Debug, Default)]
10#[serde(default, deny_unknown_fields)]
11pub struct FluxMetadata {
12    pub enabled: bool,
13    /// Enables fixpoint query caching. Saves cache in `target/FLUXCACHE`
14    pub cache: Option<bool>,
15    /// Set the default solver
16    pub solver: Option<SmtSolver>,
17    /// Enable qualifier scrapping in fixpoint
18    pub scrape_quals: Option<bool>,
19    /// Enable overflow checking
20    pub check_overflow: Option<OverflowMode>,
21    /// Enable uninterpreted casts
22    pub allow_uninterpreted_cast: Option<bool>,
23    /// Enable flux-defs to be defined as SMT functions
24    pub smt_define_fun: Option<bool>,
25    /// Set trusted to trusted
26    pub default_trusted: Option<bool>,
27    /// Set trusted to ignore
28    pub default_ignore: Option<bool>,
29    /// If present, only check files that match any of the glob patterns. Patterns are checked
30    /// relative to the location of the manifest file.
31    pub include: Option<Vec<String>>,
32    /// If present, every function in the module is implicitly labeled with a `no_panic` by default.
33    /// This means that the only way a function can panic is if it calls an external function without this attribute.
34    pub no_panic: Option<bool>,
35    /// If present, enables lean mode
36    pub lean: Option<LeanMode>,
37}
38
39impl FluxMetadata {
40    pub fn into_flags(self, target_dir: &Utf8Path, glob_prefix: Option<&Utf8Path>) -> Vec<String> {
41        let mut flags = vec![];
42        if let Some(true) = self.cache {
43            flags.push(format!("-Fcache={}", target_dir.join("FLUXCACHE")));
44        }
45        if let Some(v) = self.solver {
46            flags.push(format!("-Fsolver={v}"));
47        }
48        if let Some(v) = self.check_overflow {
49            flags.push(format!("-Fcheck-overflow={v}"));
50        }
51        if let Some(v) = self.lean {
52            flags.push(format!("-Flean={v}"));
53        }
54        if let Some(v) = self.scrape_quals {
55            flags.push(format!("-Fscrape-quals={v}"));
56        }
57        if let Some(v) = self.smt_define_fun {
58            flags.push(format!("-Fsmt-define-fun={v}"));
59        }
60        if let Some(v) = self.default_trusted {
61            flags.push(format!("-Ftrusted={v}"));
62        }
63        if let Some(v) = self.no_panic {
64            flags.push(format!("-Fno-panic={v}"));
65        }
66        if let Some(v) = self.default_ignore {
67            flags.push(format!("-Fignore={v}"));
68        }
69        if let Some(v) = self.allow_uninterpreted_cast {
70            flags.push(format!("-Fallow-uninterpreted-cast={v}"));
71        }
72        if let Some(patterns) = self.include {
73            for pat in patterns {
74                if let Some(glob_prefix) = glob_prefix
75                    && !glob_prefix.as_str().is_empty()
76                {
77                    // I haven't tested this on windows, but it should work because `globset`
78                    // will normalize patterns to use `/` as separator
79                    // don't use the empty `glob_prefix` as that makes the pattern hang off root!
80                    flags.push(format!("-Finclude={glob_prefix}/{pat}"));
81                } else {
82                    flags.push(format!("-Finclude={pat}"));
83                }
84            }
85        }
86        flags
87    }
88}
flux_bin/lib.rs

flux_bin/
lib.rs
