Module target 

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].

Functions

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_invariants_from_params 🔒

For each function parameter (and the return type), look up the type’s invariants from std-type-invariants.json and create preconditions.

collect_properties_from_named_attrs 🔒

collect_type_invariants 🔒

Look up the type path in the DB and add instantiated invariants to results.

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 🔒

instantiate_type_invariant 🔒

Create a property from a type invariant entry, substituting the parameter name.

is_drop_impl 🔒

is_numeric_field_access 🔒

Check if a string looks like a numeric field access (e.g. “0”).

is_rapx_named_attr 🔒

resolve_chain_contracts 🔒

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

type_path_key 🔒

Generate a normalised type path key for lookups in the type-invariants DB.

Type Aliases

FnContracts

A list of parsed requires contracts.

StructInvariants

A list of parsed struct invariants.