Method widen

src/analysis/memory/symbolic_value.rs:1485–1513

Returns a domain whose corresponding set of concrete values include all of the values corresponding to self and other. The set of values may be less precise (more inclusive) than the set returned by join. The chief requirement is that a small number of widen calls deterministically lead to a set of values that include of the values that could be stored in memory at the given path.

(&self, path: &Rc<Path>)

    /// deterministically lead to a set of values that include of the values that could be stored
    /// in memory at the given path.
    fn widen(&self, path: &Rc<Path>) -> Rc<SymbolicValue> {
        match &self.expression {
            Expression::CompileTimeConstant(..)
            | Expression::HeapBlock { .. }
            | Expression::Reference(..)
            | Expression::Top
            | Expression::Variable { .. }
            | Expression::Widen { .. } => self.clone(),
            _ => {
                if self.expression_size > 1000 {
                    SymbolicValue::make_from(
                        Expression::Variable {
                            path: path.clone(),
                            var_type: self.expression.infer_type(),
                        },
                        1,
                    )
                } else {
                    SymbolicValue::make_from(
                        Expression::Widen {
                            path: path.clone(),
                            operand: self.clone(),
                        },
                        3,
                    )
                }
            }
        }
    }
}