rapx/check/senryx/verification/
non_null.rs

1//! Non-null contract checker.
2//!
3//! This module verifies `NonNull` obligations against the graph's operational
4//! trace state for the object reached by a pointer or reference.
5
6use crate::check::senryx::visitor::BodyVisitor;
7
8impl<'tcx> BodyVisitor<'tcx> {
9    /// Check that a pointer's modeled target is non-null.
10    pub fn check_non_null(&self, arg: usize) -> bool {
11        let point_to_id = self.chains.get_point_to_id(arg);
12        let var_ty = self.chains.get_var_node(point_to_id);
13        if var_ty.is_none() {
14            self.show_error_info(arg);
15        }
16        var_ty.unwrap().ots.nonnull
17    }
18}