1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
//! Shared parameter/context structs for `assura check`.
use super::super::*;
/// Configuration for the `assura check` command.
pub(crate) struct CheckOptions<'a> {
pub(crate) filename: &'a str,
pub(crate) output_mode: OutputMode,
pub(crate) verbosity: Verbosity,
/// `None` means the flag was omitted. A passed value is never a sentinel.
pub(crate) layer: Option<u8>,
pub(crate) solver: Option<assura_smt::SolverChoice>,
pub(crate) watch: bool,
pub(crate) stats: bool,
pub(crate) dump_smt: Option<&'a str>,
pub(crate) show_cores: bool,
/// Unknown (incl. known limitations) and Timeout fail the check.
pub(crate) strict: bool,
/// Directory mode: only files whose header marks SHOWCASE.
pub(crate) showcase_only: bool,
/// SMT timeout in milliseconds. `None` keeps assura.toml / default.
pub(crate) timeout: Option<u64>,
}
/// Context for verification + diagnostic reporting.
pub(crate) struct VerifyContext<'a> {
pub(crate) filename: &'a str,
pub(crate) source: &'a str,
pub(crate) typed: &'a Option<assura_types::TypedFile>,
pub(crate) file: &'a Option<assura_parser::ast::SourceFile>,
pub(crate) diagnostics: &'a mut Vec<assura_diagnostics::Diagnostic>,
pub(crate) has_errors: &'a mut bool,
pub(crate) output_mode: OutputMode,
pub(crate) verbosity: Verbosity,
/// Full verify options (timeout, string_theory, parallel, etc.) with
/// layer/solver already resolved from CLI + assura.toml.
pub(crate) verify_options: assura_config::VerifyOptions,
pub(crate) show_cores: bool,
pub(crate) strict: bool,
/// Show diagnostics against this file and source instead of `filename`.
/// SMT still loads the `.ir` sidecar from `filename` (temp body IR).
pub(crate) report_file: Option<(&'a str, &'a str)>,
/// Span in `report_file`'s source for solver failures. Generated-contract
/// spans do not line up with the Rust annotation.
pub(crate) report_span: Option<std::ops::Range<usize>>,
}