Struct SenryxCheck 

pub struct SenryxCheck<'tcx> {
    pub tcx: TyCtxt<'tcx>,
    pub threshhold: usize,
}

Fields

tcx: TyCtxt<'tcx>

threshhold: usize

Implementations

impl<'tcx> SenryxCheck<'tcx>

pub fn new(tcx: TyCtxt<'tcx>, threshhold: usize) -> Self

Create a new SenryxCheck instance.

Parameters:

• tcx: compiler TyCtxt for querying types/definitions.
• threshhold: a numeric threshold used by checks.

pub fn start(&mut self, check_level: CheckLevel, is_verify: bool)

Start the checking pass over the collected functions.

• check_level controls filtering of which functions to analyze.
• is_verify toggles verification mode (vs. annotation mode).

pub fn start_analyze_std_func(&mut self)

Iterate standard library alloc functions and run verification for those that match the verification target predicate.

pub fn start_analyze_std_func_chains(&mut self)

Analyze unsafe call chains across standard library functions and print the last non-intrinsic nodes for manual inspection.

pub fn print_last_nodes(last_nodes: &HashSet<String>)

Pretty-print a set of last nodes discovered in unsafe call chains.

pub fn filter_by_check_level( tcx: TyCtxt<'tcx>, check_level: &CheckLevel, def_id: DefId, ) -> bool

Filter functions by configured check level.

• High: only publicly visible functions are considered.
• Medium/Low: accept all functions.

pub fn check_soundness( &mut self, def_id: DefId, fn_map: &FxHashMap<DefId, AAResult>, )

Run soundness checks on a single function identified by def_id using the provided alias analysis map fn_map.

pub fn annotate_safety(&self, def_id: DefId)

Collect safety annotations for def_id and display them if present.

pub fn body_visit_and_check( &mut self, def_id: DefId, fn_map: &FxHashMap<DefId, AAResult>, ) -> Vec<CheckResult>

Visit the function body and run path-sensitive checks, returning a list of CheckResults summarizing passed/failed contracts.

If the function is a method, constructor results are merged into the method’s initial state before analyzing the method body.

pub fn body_visit_and_check_uig(&self, def_id: DefId)

Variant of body_visit_and_check used for UI-guided annotation flows.

pub fn get_annotation(&self, def_id: DefId) -> HashSet<String>

Collect annotation strings for a function by scanning calls in MIR. For each call, if the callee has a safety annotation it is aggregated; otherwise the callee’s annotations (recursively) are collected.

pub fn show_check_results( tcx: TyCtxt<'tcx>, def_id: DefId, check_results: Vec<CheckResult>, )

Pretty-print aggregated check results for a function. Shows succeeded and failed contracts grouped across all arguments.

pub fn show_annotate_results( tcx: TyCtxt<'tcx>, def_id: DefId, annotation_results: HashSet<String>, )

Show annotation results for unsafe functions (diagnostic output).