in checker/src/summaries.rs [280:323]
fn extract_side_effects(
env: &Environment,
argument_count: usize,
) -> Vec<(Rc<Path>, Rc<AbstractValue>)> {
let mut heap_roots: HashSet<Rc<AbstractValue>> = HashSet::new();
let mut result = Vec::new();
for ordinal in 0..=argument_count {
let root = if ordinal == 0 {
Path::new_result()
} else {
Path::new_parameter(ordinal)
};
for (path, value) in env
.value_map
.iter()
.filter(|(p, _)| (ordinal == 0 && (**p) == root) || p.is_rooted_by(&root))
.sorted_by(|(p1, _), (p2, _)| {
let len1 = p1.path_length();
let len2 = p2.path_length();
if len1 == len2 {
if matches!(&p1.value, PathEnum::QualifiedPath { selector, .. } if **selector == PathSelector::Deref) {
Ordering::Less
} else {
Ordering::Equal
}
} else {
len1.cmp(&len2)
}
})
{
path.record_heap_blocks_and_strings(&mut heap_roots);
value.record_heap_blocks_and_strings(&mut heap_roots);
if let Expression::Variable { path: vpath, .. } | Expression::InitialParameterValue { path: vpath, ..} = &value.expression {
if ordinal > 0 && vpath.eq(path) {
// The value is not an update, but just what was there at function entry.
continue;
}
}
result.push((path.clone(), value.clone()));
}
}
extract_reachable_heap_allocations(env, &mut heap_roots, &mut result);
result
}