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)
}
}
}