Module query 

Centralized contract query service.

Provides a unified API for querying safety contracts from all sources:

1. Inline #[rapx::requires(...)] annotations — highest priority, parsed from HIR attributes.
2. #[rapx::ensures(...)] on trait methods — inherited by implementors that lack their own annotations.
3. Bundled JSON contracts — embedded backup for standard-library unsafe APIs without inline annotations.
4. Chain resolution — follows the call chain to find inherited contracts.

Contract resolution priority (per VerifyTargetCollector::get_fn_contracts): a. Inline #[rapx::requires] on the callee. b. Trait method #[rapx::requires] (if the callee is a trait impl without its own annotations). c. Bundled JSON contracts (for std callees). d. Recursive chain resolution (resolve_chain_contracts) — follows the call chain to find inherited contracts.

Functions

any_entry_to_property 🔒

Parse an any disjunction entry from JSON into a Property::Or property.

entry_to_property

Convert a single PropertyEntry from JSON into the properties it denotes.

is_contract_token_char 🔒

normalize_json_contract_arg

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

query_json_contracts

Query contracts for a function from the bundled JSON backup database.

resolve_json_args

Resolve JSON contract argument strings to parsed syn::Expr values.

resolve_json_param_name

Resolve a simple parameter-name reference in a JSON contract arg string to the arg:N positional form. Complex expressions (containing function calls, field access, etc.) are left unchanged — they are handled later by the expression parser which already knows how to resolve named parameters.

scan_while 🔒