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 overflow checking
20    pub smt_define_fun: Option<bool>,
21    /// Set trusted trusted
22    pub default_trusted: Option<bool>,
23    /// Set trusted ignore
24    pub default_ignore: Option<bool>,
25}
26
27impl FluxMetadata {
28    pub fn into_flags(self, target_dir: &Utf8Path) -> Vec<String> {
29        let mut flags = vec![];
30        if let Some(true) = self.cache {
31            flags.push(format!("-Fcache={}", target_dir.join("FLUXCACHE")));
32        }
33        if let Some(v) = self.solver {
34            flags.push(format!("-Fsolver={v}"));
35        }
36        if let Some(v) = self.check_overflow {
37            flags.push(format!("-Fcheck-overflow={v}"));
38        }
39        if let Some(v) = self.scrape_quals {
40            flags.push(format!("-Fscrape-quals={v}"));
41        }
42        if let Some(v) = self.smt_define_fun {
43            flags.push(format!("-Fsmt-define-fun={v}"));
44        }
45        if let Some(v) = self.default_trusted {
46            flags.push(format!("-Ftrusted={v}"));
47        }
48        if let Some(v) = self.default_ignore {
49            flags.push(format!("-Fignore={v}"));
50        }
51        flags
52    }
53}
flux_bin/lib.rs

flux_bin/
lib.rs
