Module union_find 

Union-Find (Disjoint Set Union) data structure for call graph connectivity.

Invariants (Creusot)

#[invariant(self.parent.len() == self.rank.len())]
#[invariant(forall(|i| i < self.parent.len() ==> self.parent[i] < self.parent.len()))]

Properties

• find is idempotent: find(find(x)) == find(x)
• merge establishes equivalence: after merge(x, y), find(x) == find(y)
• component_count returns the number of distinct roots among file-kind nodes

Structs

NodeDescriptor

Descriptor for a node in the call graph.

UnionFind

Union-Find data structure for tracking connected components in a call graph.

Enums

NodeKind

The kind of node in the call graph.