rapx/check/senryx/verification/
typed.rs

1//! Type-compatibility contract checker.
2//!
3//! This module verifies `Typed` obligations by comparing the graph's current
4//! object type with the pointer node's tracked type and then requiring
5//! initialization for the reached value.
6
7use crate::{analysis::utils::fn_info::is_strict_ty_convert, check::senryx::visitor::BodyVisitor};
8
9impl<'tcx> BodyVisitor<'tcx> {
10    /// Check whether the value the pointer reaches is valid for its tracked type.
11    pub fn check_typed(&self, arg: usize) -> bool {
12        let obj_ty = self.chains.get_obj_ty_through_chain(arg).unwrap();
13        let var = self.chains.get_var_node(arg);
14        let var_ty = var.unwrap().ty.unwrap();
15        if obj_ty != var_ty && is_strict_ty_convert(self.tcx, obj_ty, var_ty) {
16            return false;
17        }
18        self.check_init(arg)
19    }
20}