Struct AnalyzeOptions 

pub struct AnalyzeOptions {

    pub file_label: String,
    pub module_base_dir: Option<String>,
    pub loaded_modules: Option<Vec<LoadedModule>>,
    pub include_intent_warnings: bool,
    pub include_coverage_warnings: bool,
    pub include_law_dependency_warnings: bool,
    pub include_cse_warnings: bool,
    pub include_perf_warnings: bool,
    pub include_independence_warnings: bool,
    pub include_naming_warnings: bool,
    pub include_non_tail_warnings: bool,
    pub include_unused_bindings: bool,
    pub include_verify_run: bool,
    pub include_why_summary: bool,
    pub include_context_summary: bool,
}

Options for analyze_source. Defaults enable every available collector.

Fields

file_label: String

module_base_dir: Option<String>

loaded_modules: Option<Vec<LoadedModule>>

Pre-resolved dependency modules (e.g. from a virtual filesystem in the playground). When set, takes precedence over module_base_dir — the type checker integrates these directly instead of loading from disk.

include_intent_warnings: bool

include_coverage_warnings: bool

include_law_dependency_warnings: bool

include_cse_warnings: bool

include_perf_warnings: bool

include_independence_warnings: bool

include_naming_warnings: bool

include_non_tail_warnings: bool

include_unused_bindings: bool

include_verify_run: bool

When true and the runtime feature is enabled, execute every verify block found in the source and emit a diagnostic per failing case. Off by default: analysis should stay pure static checks; callers opt in explicitly.

include_why_summary: bool

When true, populate AnalysisReport::why_summary with per-function justification data. Off by default.

include_context_summary: bool

When true, populate AnalysisReport::context_summary with module shape / function / type / decision summary.

Implementations

impl AnalyzeOptions

pub fn new(file_label: impl Into<String>) -> Self

pub fn with_module_base_dir(self, dir: impl Into<String>) -> Self

pub fn with_loaded_modules(self, loaded: Vec<LoadedModule>) -> Self

Trait Implementations

impl Clone for AnalyzeOptions

fn clone(&self) -> AnalyzeOptions

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for AnalyzeOptions

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for AnalyzeOptions

fn default() -> Self

Returns the “default value” for a type.