Module target 

Discovery of verification targets and their contract obligations.

VerifyTargetCollector walks the crate’s HIR (in targeted or scan mode), and for each candidate assembles a FunctionTarget: unsafe call-site checkpoints with per-callee preconditions, raw-pointer/static-mut synthetic checkpoints, struct invariants, and std type invariants.

Structs

FunctionTarget 🔒

Collected verification data for a single function under analysis.

PrepareTargets 🔒

Analysis pass that finds all verification targets.

StructTarget 🔒

Collected verification data for a struct that owns methods marked with #[rapx::verify].

TraitEnsurance 🔒

Collected verification data for an impl unsafe Trait for Type block.

VerifyTargetCollector 🔒

Visitor that collects targets annotated with #[rapx::verify].

Enums

MarkerTraitKind 🔒

Which marker trait an unsafe impl is claiming safety for.

TraitEnsuranceKind 🔒

What a TraitEnsurance must verify.

Functions

bind_alive_regions 🔒

Bind Alive(p, 'a) region idents in a contract to Regions, resolving 'a against def_id (the item that declares 'a: the struct for its invariants, the function for its requires).

build_marker_trait_obligations 🔒

Generate the type-level ensures obligations for a marker-trait impl from the bundled std-trait-ensures.json template, substituting ty:Self with the implementing type.

build_raw_ptr_deref_checks 🔒

Build (pseudo-checkpoint, properties) pairs for every raw pointer dereference in the target function.

build_static_mut_checks 🔒

Build (pseudo-checkpoint, properties) pairs for every static mut access in the target function.

build_type_atom 🔒

Build a single type-level obligation from a std-trait-ensures.json entry, substituting ty:Self with self_ty. Supports the any disjunction and falls back to named compound properties (expand_compound) for tags that are not built-in primitives.

call_arg_to_outer_param 🔒

Trace a call-site argument operand back to the enclosing callee’s parameter index (0-based), following direct Copy/Move assignment chains. Returns None for constants, field projections, call results, or values that do not trace to a parameter (those references cannot be restated on the enclosing callee).

collect_properties_from_named_attrs 🔒

extract_tamed_field 🔒

The raw-pointer field name a struct declares via #[rapx::invariant(Allocated(field))] or #[rapx::invariant(Owning(field))], used to bind a TamedRawPtr compound’s Ptr parameter.

get_contract_from_annotation 🔒

Parses requires contracts from source-level RAPx annotations attached to a definition.

get_struct_invariants_from_annotation 🔒

Parses struct invariants from source-level RAPx annotations attached to a struct definition.

get_trait_contracts_from_annotation 🔒

Parses trait safety contracts from #[rapx::ensures(...)] on unsafe trait methods, grouped by method name.

get_trait_method_requires 🔒

is_drop_impl 🔒

is_rapx_named_attr 🔒

marker_trait_kind 🔒

Resolve whether an unsafe impl is implementing the Send/Sync marker trait.

rebind_expr 🔒

rebind_place 🔒

rebind_property_arg 🔒

rebind_property_to_args 🔒

Rewrite a contract’s argument references (PlaceBase::Arg(i)) onto the enclosing callee’s parameters using the call-site argument list. This rebinds a leaf callee’s contract (e.g. ptr::write’s ValidPtr(self, T, 1)) to the wrapper callee’s arguments (e.g. maybe_init_slot’s ptr).

rebind_ty 🔒

Replace a leaf callee’s type parameter (TyKind::Param) with the concrete type argument passed at the call site.

resolve_chain_contracts 🔒

Follow an unsafe callee’s call chain to find inherited safety contracts.

Type Aliases

FnContracts 🔒

A list of parsed requires contracts.

StructInvariants 🔒

A list of parsed struct invariants.