Module visitor 

Backward path visitor — walks a finite path backward from a checkpoint and keeps only MIR items that can affect the required property.

The def-use layer lives in super::super::def_use; this module focuses on the path-level control flow decisions: calls, SCC exits, and path-condition branches.

Structs

BackwardSlicer 🔒

Entry point for backward path visiting.

Functions

collect_flow_uses 🔒

Collect the source locals of the dataflow edges entering (block, statement_index) from the def locals of defs.

collect_statement_uses 🔒

Collect all place-uses for a statement from dataflow edges and operands.

needs_invalidation_tracking 🔒

Whether a property’s checker reads allocation liveness (alloc.facts.dead), so the backward slice must keep StorageDead/StorageLive/Drop unconditionally (the allocation owner may not be reachable from the pointer target, e.g. a raw pointer into a separately-owned Vec/Box buffer).

statement_can_refine 🔒

terminator_is_path_condition 🔒