Method equals

src/analysis/memory/symbolic_value.rs:793–846

Returns an element that is "self == other".

(&self, other: Rc<SymbolicValue>)

    /// Returns an element that is "self == other".
    fn equals(&self, other: Rc<SymbolicValue>) -> Rc<SymbolicValue> {
        match (&self.expression, &other.expression) {
            (Expression::CompileTimeConstant(v1), Expression::CompileTimeConstant(v2)) => {
                return Rc::new(v1.equals(v2).into());
            }
            // If self and other are the same location in memory, return true unless the value might be NaN.
            (
                Expression::Variable {
                    path: p1,
                    var_type: _t1,
                },
                Expression::Variable {
                    path: p2,
                    var_type: _t2,
                },
            ) => {
                if p1 == p2 {
                    return Rc::new(SymbolicValue::new_true());
                }
            }
            // [!x == 0] -> x when x is Boolean. Canonicalize it to the latter.
            (
                Expression::LogicalNot { operand },
                Expression::CompileTimeConstant(ConstantValue::Int(val)),
            ) => {
                if *val == 0 && operand.expression.infer_type() == ExpressionType::Bool {
                    return operand.clone();
                }
            }
            // [x == 0] -> !x when x is a Boolean. Canonicalize it to the latter.
            // [x == 1] -> x when x is a Boolean. Canonicalize it to the latter.
            (x, Expression::CompileTimeConstant(ConstantValue::Int(val))) => {
                if x.infer_type() == ExpressionType::Bool {
                    if *val == 0 {
                        return self.logical_not();
                    } else if *val == 1 {
                        return self.clone();
                    }
                }
            }
            (x, y) => {
                // If self and other are the same expression and the expression could not result in NaN
                // and the expression represents exactly one value, we can simplify this to true.
                if x == y {
                    return Rc::new(SymbolicValue::new_true());
                }
            }
        }
        // Return an equals expression rather than a constant expression.
        SymbolicValue::make_binary(self.clone(), other, |left, right| Expression::Equals {
            left,
            right,
        })
    }

    /// Returns an element that is "self >= other".
    fn greater_or_equal(&self, other: Rc<SymbolicValue>) -> Rc<SymbolicValue> {