Module verifier 

Forward visitor for relevant MIR items.

This module consumes the MIR items produced by backward_visit and visits them in path order. The current implementation is a skeleton: it records simple value/fact summaries and leaves unsupported MIR effects as notes so later property checkers can be added incrementally.

Structs

CallSummary

Summary for a retained call terminator.

ForwardVerifier

Visits relevant MIR items forward and builds an abstract state.

ForwardVisitResult

Result produced by visiting relevant MIR items forward.

ValueDefinition

One local definition observed while replaying retained MIR items.

Enums

AbstractValue

Abstract value assigned to a MIR local by the forward visitor.

ForwardStep

One step visited by the forward visitor.

StateFact

Fact recorded from a relevant MIR item.

Functions

aggregate_name 🔒

Return a compact aggregate kind name.

align_guard_value 🔒

allocation_object_for_source 🔒

chosen_successor 🔒

Return the next MIR block after block in a finite verification path.

chosen_switch_value 🔒

Return the concrete SwitchInt value that selects the next path block.

const_int_from_debug 🔒

Extract a small integer constant from rustc’s debug representation.

const_int_value 🔒

copy_chain_places 🔒

extract_const_param_name 🔒

find_cmp_source 🔒

fixed_allocation_elements 🔒

is_const_zero 🔒

is_power_of_two 🔒

known_alignment_of 🔒

maybe_uninit_inner_ty_name 🔒

operand_place 🔒

Convert an operand into a place key when it names a MIR place.

resolve_value_chain 🔒

value_from_operand 🔒

Convert a MIR operand to an abstract value.