Module def_use 

Def-use computation for the backward path visitor.

These types and helpers track which MIR places are relevant to a safety property and compute definitions/uses from MIR terminators. This is the data layer that slicing drives block-by-block along a finite verification path; keeping it separate lets the core visit logic stay focused on path-level decisions (calls, SCC exits, path conditions).

Structs

DefUse

Definitions and uses collected from one MIR item.

PlaceKey

Projection-insensitive enough place key for relevance tracking.

RelevantPlaces

Set of places that make MIR items relevant to a property.

Enums

PlaceBaseKey

Base of a contract/MIR place tracked by relevance.

Functions

bind_callsite_roots

Bind callee parameter roots to concrete MIR call operands.

bind_operand_place 🔒

call_args_uses_at

Collect MIR roots used by selected call argument indices.

is_target_argument_index 🔒

Return whether an argument index is a target-place position for a property.

operand_uses

Collect all MIR roots used by an operand.

place_projection_uses

Collect only the index roots used by a place projection.

place_uses

Collect the base and projection-index roots used by a MIR place.

rvalue_operands

Collect all MIR operands referenced by an rvalue.

terminator_use_def

Collect definitions and uses for one MIR terminator.