flux_bin/
lib.rs

1use cargo_metadata::camino::Utf8Path;
2use flux_config::{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}
33
34impl FluxMetadata {
35    pub fn into_flags(self, target_dir: &Utf8Path, glob_prefix: Option<&Utf8Path>) -> Vec<String> {
36        let mut flags = vec![];
37        if let Some(true) = self.cache {
38            flags.push(format!("-Fcache={}", target_dir.join("FLUXCACHE")));
39        }
40        if let Some(v) = self.solver {
41            flags.push(format!("-Fsolver={v}"));
42        }
43        if let Some(v) = self.check_overflow {
44            flags.push(format!("-Fcheck-overflow={v}"));
45        }
46        if let Some(v) = self.scrape_quals {
47            flags.push(format!("-Fscrape-quals={v}"));
48        }
49        if let Some(v) = self.smt_define_fun {
50            flags.push(format!("-Fsmt-define-fun={v}"));
51        }
52        if let Some(v) = self.default_trusted {
53            flags.push(format!("-Ftrusted={v}"));
54        }
55        if let Some(v) = self.default_ignore {
56            flags.push(format!("-Fignore={v}"));
57        }
58        if let Some(v) = self.allow_uninterpreted_cast {
59            flags.push(format!("-Fallow-uninterpreted-cast={v}"));
60        }
61        if let Some(patterns) = self.include {
62            for pat in patterns {
63                if let Some(glob_prefix) = glob_prefix
64                    && !glob_prefix.as_str().is_empty()
65                {
66                    // I haven't tested this on windows, but it should work because `globset`
67                    // will normalize patterns to use `/` as separator
68                    // don't use the empty `glob_prefix` as that makes the pattern hang off root!
69                    flags.push(format!("-Finclude={glob_prefix}/{pat}"));
70                } else {
71                    flags.push(format!("-Finclude={pat}"));
72                }
73            }
74        }
75        flags
76    }
77}