fn uses()

in checker/src/abstract_value.rs [6785:6870]


    fn uses(&self, variables: &HashSet<Rc<Path>>) -> bool {
        match &self.expression {
            Expression::Bottom => false,
            Expression::Top => true,
            Expression::Add { left, right }
            | Expression::AddOverflows { left, right, .. }
            | Expression::And { left, right }
            | Expression::BitAnd { left, right }
            | Expression::BitOr { left, right }
            | Expression::BitXor { left, right }
            | Expression::Div { left, right }
            | Expression::Equals { left, right }
            | Expression::GreaterOrEqual { left, right }
            | Expression::GreaterThan { left, right }
            | Expression::IntrinsicBinary { left, right, .. }
            | Expression::LessOrEqual { left, right }
            | Expression::LessThan { left, right }
            | Expression::Mul { left, right }
            | Expression::MulOverflows { left, right, .. }
            | Expression::Ne { left, right }
            | Expression::Offset { left, right }
            | Expression::Or { left, right }
            | Expression::Rem { left, right }
            | Expression::Shl { left, right }
            | Expression::ShlOverflows { left, right, .. }
            | Expression::Shr { left, right, .. }
            | Expression::ShrOverflows { left, right, .. }
            | Expression::Sub { left, right }
            | Expression::SubOverflows { left, right, .. } => {
                left.uses(variables) || right.uses(variables)
            }
            Expression::BitNot { operand, .. }
            | Expression::Cast { operand, .. }
            | Expression::IntrinsicBitVectorUnary { operand, .. }
            | Expression::IntrinsicFloatingPointUnary { operand, .. }
            | Expression::Neg { operand }
            | Expression::LogicalNot { operand }
            | Expression::TaggedExpression { operand, .. }
            | Expression::Transmute { operand, .. }
            | Expression::UnknownTagCheck { operand, .. } => operand.uses(variables),
            Expression::CompileTimeConstant(..) => false,
            Expression::ConditionalExpression {
                condition,
                consequent,
                alternate,
            } => {
                condition.uses(variables) || consequent.uses(variables) || alternate.uses(variables)
            }
            Expression::HeapBlock { .. } => false,
            Expression::HeapBlockLayout {
                length, alignment, ..
            } => length.uses(variables) || alignment.uses(variables),
            Expression::Join { left, right } => left.uses(variables) || right.uses(variables),
            Expression::Memcmp {
                left,
                right,
                length,
            } => left.uses(variables) || right.uses(variables) || length.uses(variables),
            Expression::Reference(path)
            | Expression::InitialParameterValue { path, .. }
            | Expression::UnknownTagField { path }
            | Expression::Variable { path, .. } => variables.contains(path),
            Expression::Switch {
                discriminator,
                cases,
                default,
            } => {
                discriminator.uses(variables)
                    || default.uses(variables)
                    || cases.iter().any(|(case_val, result_val)| {
                        case_val.uses(variables) || result_val.uses(variables)
                    })
            }
            Expression::UninterpretedCall {
                callee,
                arguments: args,
                ..
            } => callee.uses(variables) || args.iter().any(|arg| arg.uses(variables)),
            Expression::UnknownModelField { path, default } => {
                variables.contains(path) || default.uses(variables)
            }
            Expression::WidenedJoin { operand, path } => {
                operand.uses(variables) || variables.contains(path)
            }
        }
    }