Module target 

Structs

FunctionTarget

Collected verification data for a function annotated with #[rapx::verify].

PrepareTargets

Analysis pass that finds all targets annotated with #[rapx::verify].

StructTarget

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

VerifyTargetCollector

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

Functions

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.

is_rapx_requires_attr 🔒

Returns whether an attribute is exactly #[rapx::requires(...)].

Type Aliases

FnContracts

A list of parsed requires contracts.

StructInvariants

A list of parsed struct invariants.