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

builtin_models 🔒

Builtin call models: API behaviour modelling when MIR is unavailable.

interprocedural 🔒

Interprocedural call summaries derived from MIR for local wrapper functions.

Structs

CallContext 🔒

Caller constraints that affect a callee’s path feasibility, propagated down the call chain during must-write summarization. Only concrete literal arguments are carried for now; symbolic path conditions come later.

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.

from_raw_parts_elem_size 🔒

Element size of a from_raw_parts result. Covers &[T]/*[T] (borrowed slice) and Vec<T> (owned); String and unknown layouts fall back to 1 (String’s element is u8, so 1 is correct).

from_raw_parts_elem_ty 🔒

Element type of a from_raw_parts result: &[T]/*[T]/Vec<T> yield T; other types (including String) return None.

is_maybe_dangling 🔒

Whether did is the MaybeDangling lang item.

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:

vec_elem_ty 🔒

Element type of a Vec<T>, if ty is a Vec.