rapx/check/senryx/verification/
init.rs

1//! Initialization contract checker.
2//!
3//! This module verifies `Init`-style obligations from graph OTS state. For
4//! aggregate nodes it recursively checks modeled field nodes; for leaves it uses
5//! the node's `init` flag.
6
7use crate::check::senryx::visitor::BodyVisitor;
8
9impl<'tcx> BodyVisitor<'tcx> {
10    /// Check each field's init state in the graph tree, or the node itself for leaves.
11    pub fn check_init(&self, arg: usize) -> bool {
12        let point_to_id = self.chains.get_point_to_id(arg);
13        let var = self.chains.get_var_node(point_to_id).unwrap();
14        if !var.field.is_empty() {
15            let mut init_flag = true;
16            for field in &var.field {
17                init_flag &= self.check_init(*field.1);
18            }
19            init_flag
20        } else {
21            var.ots.init
22        }
23    }
24}

rapx/check/senryx/verification/init.rs

rapx/check/senryx/verification/
init.rs