Method check_overflow

src/checker/assertion_checker.rs:240–285

(
        &mut self,
        value: Rc<SymbolicValue>,
        expected: bool,
        abstract_value: &AbstractDomain<DomainType>,
    )

    }

    fn check_overflow(
        &mut self,
        value: Rc<SymbolicValue>,
        expected: bool,
        abstract_value: &AbstractDomain<DomainType>,
    ) -> CheckerResult {
        match &value.expression {
            Expression::CompileTimeConstant(ConstantValue::Int(constant)) => {
                if constant == &Integer::from(expected) {
                    CheckerResult::Safe
                } else {
                    CheckerResult::Unsafe
                }
            }
            Expression::Variable { path, var_type } => {
                assert_eq!(*var_type, ExpressionType::Bool);
                match &path.value {
                    // Overflow operand is a qualified path, meaning that it is the compiler generated bit indicating overflow: `path.1`
                    // The value is in `path.0`, so we construct it manually and test whether its value is possibly an overflow
                    PathEnum::QualifiedPath {
                        length: _,
                        qualifier,
                        selector,
                    } => {
                        if Rc::new(PathSelector::Field(1)) != *selector {
                            CheckerResult::Warning
                        } else {
                            let new_path = Path::new_field(qualifier.clone(), 0);
                            if let Some(&rustc_type) =
                                self.body_visitor.type_visitor.path_ty_cache.get(&new_path)
                            {
                                self.check_within_range(new_path, rustc_type, abstract_value)
                            } else {
                                CheckerResult::Warning
                            }
                        }
                    }
                    _ => {
                        // Overflow operand is not a qualified path, meaning that we can test it directly
                        self.check_assert_condition(value, expected, abstract_value)
                    }
                }
            }
            _ => self.check_assert_condition(value, expected, abstract_value),
        }
    }
}