flux_bin/
lib.rs

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

flux_bin/
lib.rs
