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 pub cache: Option<bool>,
13 pub solver: Option<SmtSolver>,
15 pub scrape_quals: Option<bool>,
17 pub check_overflow: Option<bool>,
19 pub allow_uninterpreted_cast: Option<bool>,
21 pub smt_define_fun: Option<bool>,
23 pub default_trusted: Option<bool>,
25 pub default_ignore: Option<bool>,
27 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 flags.push(format!("-Finclude={glob_prefix}/{pat}"));
65 } else {
66 flags.push(format!("-Finclude={pat}"));
67 }
68 }
69 }
70 flags
71 }
72}