Method logical_not

src/analysis/memory/symbolic_value.rs:1047–1096

Returns an element that is "!self" where self is a bool.

(&self)

    /// Returns an element that is "!self" where self is a bool.
    fn logical_not(&self) -> Rc<SymbolicValue> {
        if let Expression::CompileTimeConstant(v1) = &self.expression {
            let result = v1.logical_not();
            if result != ConstantValue::Bottom {
                return Rc::new(result.into());
            }
        };
        match &self.expression {
            Expression::Bottom => self.clone(),
            Expression::Equals { left: x, right: y } if x.expression.infer_type().is_integer() => {
                // [!(x == y)] -> x != y
                x.not_equals(y.clone())
            }
            Expression::GreaterThan { left: x, right: y }
                if x.expression.infer_type().is_integer() =>
            {
                // [!(x > y)] -> x <= y
                x.less_or_equal(y.clone())
            }
            Expression::GreaterOrEqual { left: x, right: y }
                if x.expression.infer_type().is_integer() =>
            {
                // [!(x >= y)] -> x < y
                x.less_than(y.clone())
            }
            Expression::LessThan { left: x, right: y }
                if x.expression.infer_type().is_integer() =>
            {
                // [!(x < y)] -> x >= y
                x.greater_or_equal(y.clone())
            }
            Expression::LessOrEqual { left: x, right: y }
                if x.expression.infer_type().is_integer() =>
            {
                // [!(x <= y)] -> x > y
                x.greater_than(y.clone())
            }
            Expression::LogicalNot { operand } => {
                // [!!x] -> x
                operand.clone()
            }
            Expression::Ne { left: x, right: y } if x.expression.infer_type().is_integer() => {
                // [!(x != y)] -> x == y
                x.equals(y.clone())
            }
            _ => SymbolicValue::make_unary(self.clone(), |operand| Expression::LogicalNot {
                operand,
            }),
        }
    }

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