Module call_summary 

Interprocedural call summaries for the staged verifier.

The backward visitor needs dependency information: when a call result is relevant, which call arguments should become relevant too? The forward visitor needs effect information: after a retained call, what facts about the return value or arguments can be added or forgotten?

This module keeps those summaries in one place. Standard unsafe/std APIs are summarized by name. Local callees can additionally use the existing dataflow graph to approximate which arguments flow into the return value.

Modules

fn_simulator

Function simulation: API behaviour modelling when MIR is unavailable.

interprocedural

Structs

CallDependencySummary

Dependency summary consumed by the backward visitor.

CallEffectSummary

Effect summary consumed by the forward visitor.

Enums

CallEffect

Path-local effect produced by a retained call.

Functions

dependency_summary

Return dependency information for a MIR call terminator.

effect_summary

Return effect information for a MIR call terminator.

transparent_deref_peel 🔒

Detect a transparent-wrapper deref whose receiver is ManuallyDrop<T> or MaybeDangling<T>, and return how many leading field-0 hops must be peeled to reach the inner T: