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 flux-defs to be defined as SMT functions
20    pub smt_define_fun: Option<bool>,
21    /// Set trusted to trusted
22    pub default_trusted: Option<bool>,
23    /// Set trusted to ignore
24    pub default_ignore: Option<bool>,
25    /// If present, only check files that match any of the glob patterns. Patterns are checked
26    /// relative to the location of the manifest file.
27    pub include: Option<Vec<String>>,
28}
29
30impl FluxMetadata {
31    pub fn into_flags(self, target_dir: &Utf8Path, glob_prefix: Option<&Utf8Path>) -> Vec<String> {
32        let mut flags = vec![];
33        if let Some(true) = self.cache {
34            flags.push(format!("-Fcache={}", target_dir.join("FLUXCACHE")));
35        }
36        if let Some(v) = self.solver {
37            flags.push(format!("-Fsolver={v}"));
38        }
39        if let Some(v) = self.check_overflow {
40            flags.push(format!("-Fcheck-overflow={v}"));
41        }
42        if let Some(v) = self.scrape_quals {
43            flags.push(format!("-Fscrape-quals={v}"));
44        }
45        if let Some(v) = self.smt_define_fun {
46            flags.push(format!("-Fsmt-define-fun={v}"));
47        }
48        if let Some(v) = self.default_trusted {
49            flags.push(format!("-Ftrusted={v}"));
50        }
51        if let Some(v) = self.default_ignore {
52            flags.push(format!("-Fignore={v}"));
53        }
54        if let Some(patterns) = self.include {
55            for pat in patterns {
56                if let Some(glob_prefix) = glob_prefix {
57                    // I haven't tested this on windows, but it should work because `globset`
58                    // will normalize patterns to use `/` as separator
59                    flags.push(format!("-Finclude={glob_prefix}/{pat}"));
60                } else {
61                    flags.push(format!("-Finclude={pat}"));
62                }
63            }
64        }
65        flags
66    }
67}
flux_bin/lib.rs

flux_bin/
lib.rs
