Struct FunctionTarget 

pub struct FunctionTarget<'tcx> {
    pub def_id: DefId,
    pub owner_struct_def_id: Option<DefId>,
    pub checkpoints: Vec<Checkpoint<'tcx>>,
    pub callee_requires: HashMap<DefId, FnContracts<'tcx>>,
    pub caller_requires: FnContracts<'tcx>,
    pub struct_invariants: Vec<Property<'tcx>>,
    pub raw_ptr_deref_checks: Vec<(Checkpoint<'tcx>, Vec<Property<'tcx>>)>,
    pub static_mut_checks: Vec<(Checkpoint<'tcx>, Vec<Property<'tcx>>)>,
}

Collected verification data for a single function under analysis.

FunctionTarget is the complete problem statement for one function: it records every unsafe operation found in the function’s MIR body, the safety contracts that each operation demands, and any contracts or invariants that serves as entry assumptions or structural guarantees.

How it is built

VerifyTargetCollector::build_function_target assembles a FunctionTarget in one pass over the MIR body:

1. Unsafe checkpoints are collected via collect_unsafe_callsites.
2. Each unique callee DefId gets its #[rapx::requires] contracts parsed (with fallback to bundled JSON contracts for standard-library callees).
3. Raw pointer dereferences are detected and converted into synthetic (pseudo-checkpoint, [ValidPtr, Align, (Typed)]) pairs.
4. The caller’s own #[rapx::requires] contracts become entry assumptions.
5. If the function is a method on a struct, struct-level #[rapx::invariant] and #[rapx::requires] annotations are collected.

Role in the pipeline

The VerifyDriver consumes a FunctionTarget to route each unsafe operation to the verifier engine along reachability paths extracted from the MIR CFG. The target is the primary data carrier between the target collection stage and the path extraction / verification stage.

Fields

def_id: DefId

The function being verified.

owner_struct_def_id: Option<DefId>

Owning struct when this function is an associated method (e.g. impl MyStruct { fn foo(...) }). None for free functions.

Used to associate struct invariants and to group method-level verification results under the owning struct in diagnostic output.

checkpoints: Vec<Checkpoint<'tcx>>

All call-terminator-based unsafe checkpoints found in this function’s MIR.

Each Checkpoint records the callee DefId, the source-span of the call, the basic-block location, and the MIR operands passed as arguments.

callee_requires: HashMap<DefId, FnContracts<'tcx>>

Safety contracts demanded by each unique unsafe callee reachable from this function, keyed by callee DefId.

Contracts are sourced from #[rapx::requires(...)] annotations on the callee (inline mode) or from a bundled JSON contract database for standard-library functions. Each value is a Vec<Property> — the concrete safety requirements the callee expects its caller to satisfy.

caller_requires: FnContracts<'tcx>

Safety contracts that the caller itself requires as entry assumptions, parsed from #[rapx::requires(...)] on this function.

During verification the engine prepends these properties as facts that are assumed to hold at function entry, constraining the backward data-dependency analysis and forward simulation.

struct_invariants: Vec<Property<'tcx>>

Struct invariants that methods of the owning struct must maintain.

Collected from #[rapx::invariant(...)] / #[rapx::requires(...)] annotations on the struct definition. Checked at constructor return blocks and at all path endpoints for non-constructor methods.

raw_ptr_deref_checks: Vec<(Checkpoint<'tcx>, Vec<Property<'tcx>>)>

Raw pointer dereference checks with their required safety properties.

Each entry is a (Checkpoint, Vec<Property>) pair where the Checkpoint carries a synthetic dummy DefId (so the path extractor can treat dereferences uniformly with checkpoints) and the properties encode the pointer-validity requirements: always ValidPtr and Align; additionally Typed when the dereference is a read.

static_mut_checks: Vec<(Checkpoint<'tcx>, Vec<Property<'tcx>>)>

Static mut access checks with their required safety properties.

Each entry is a (Checkpoint, Vec<Property>) pair following the same pattern as raw_ptr_deref_checks. The properties are ValidPtr, Align, and Init (conservatively checked for both reads and writes).

Trait Implementations

impl<'tcx> Clone for FunctionTarget<'tcx>

fn clone(&self) -> FunctionTarget<'tcx>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.