assura 0.5.0

Contract-first AI-native language. Write what it should do. AI proves it does.
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

//! 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,
    pub(crate) layer: 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>>,
}