Method check_within_range

src/checker/assertion_checker.rs:193–238

(
        &self,
        path: Rc<Path>,
        val_ty: Ty<'tcx>,
        abstract_value: &AbstractDomain<DomainType>,
    )

    }

    pub fn check_within_range(
        &self,
        path: Rc<Path>,
        val_ty: Ty<'tcx>,
        abstract_value: &AbstractDomain<DomainType>,
    ) -> CheckerResult {
        let solver = &self.body_visitor.z3_solver;
        Self::add_numerical_constraints(&solver, abstract_value);

        let exp_type: ExpressionType = val_ty.kind().into();

        // First solve `var <= max` and `var >= min`
        let mut exp = LinearExpression::default();
        exp = exp - exp_type.max_value_int() + path.clone();
        let cst1 = LinearConstraint::LessEq(exp);

        let mut exp = LinearExpression::default();
        exp = exp + exp_type.min_value_int() - path;
        let cst2 = LinearConstraint::LessEq(exp);

        let within_range_cond = solver.make_and_z3_expression(&cst1, &cst2);

        let result;
        match solver.solve_expression(&within_range_cond) {
            SmtResult::Unsat => {
                // value is not within the valid range
                result = CheckerResult::Unsafe;
            }
            SmtResult::Sat => {
                // value may be within the valid range, now check whether `not within the range` is always false
                if solver.solve_expression(&solver.make_not_z3_expression(within_range_cond))
                    == SmtResult::Unsat
                {
                    // `not within the range` is always false, so `value is within the range` is always true
                    result = CheckerResult::Safe;
                } else {
                    result = CheckerResult::Warning;
                }
            }
            SmtResult::Unknown => {
                result = CheckerResult::Warning;
            }
        }
        solver.reset();
        result
    }

    fn check_overflow(
        &mut self,