fn extract_side_effects()

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
}