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.

collect_properties_from_ensures_attrs 🔒

Collects properties from #[rapx::ensures(...)] attributes.

collect_properties_from_invariant_attrs 🔒

Collects properties from #[rapx::invariant(...)] attributes.

collect_properties_from_named_attrs 🔒

collect_properties_from_requires_attrs 🔒

Collects properties from #[rapx::requires(...)] attributes.

get_contract_from_annotation 🔒

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

get_contract_from_entry 🔒

Builds contracts from backup JSON entries.

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

is_rapx_named_attr 🔒

normalize_json_contract_arg 🔒

Convert explicit JSON contract tokens into the expression syntax accepted by the existing property parser.

resolve_chain_contracts 🔒

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

scan_while 🔒

Type Aliases

FnContracts

A list of parsed requires contracts.

StructInvariants

A list of parsed struct invariants.