Functions§
- access_
ident_ recursive - return the (ident, its fields) of the expr.
- check_
safety - check_
visibility - dfs_
find_ 🔒unsafe_ chains - display_
hashmap - extract_
unsafe_ 🔒callee - find_
generic_ 🔒in_ ty - Iterate the args’ types recursively and find the matched generic one.
- find_
generic_ 🔒param - Find generic type parameters in the parameter list
- find_
unsafe_ 🔒callees_ in_ function - generate_
contract_ from_ annotation - Get the annotation in tag-std style. Then generate the contractual invariant states (CIS) for the args. This function will recognize the args name and record states to MIR variable (represent by usize). Return value means Vec<(local_id, fields of this local, contracts)>
- generate_
contract_ from_ annotation_ without_ field_ types - Same with
generate_contract_from_annotationbut does not contain field types. - generate_
node_ ty - get_
adt_ def_ id_ by_ adt_ method - get_
adt_ ty - get_
all_ callees - get_
all_ mutable_ methods - get_
all_ std_ fns_ by_ rustc_ public - get_
all_ std_ unsafe_ callees - get_
all_ std_ unsafe_ callees_ block_ id - get_
all_ std_ unsafe_ chains - get_
callees - get_
cleaned_ def_ path_ name - get_
cleaned_ def_ path_ name_ ori - get_
cons - get_
impl_ items_ of_ struct - get_
impls_ for_ struct - get_
known_ 🔒std_ names - We use a json to record known std apis’ arg names. This function will search the json and return the names. Notes: If std gets updated, the json may still record old ones.
- get_
pointee - get_
public_ fields - get_sp
- get_
sp_ json - get_
std_ api_ signature_ json - get_
struct_ name - get_
type - has_
mut_ self_ param - has_
tainted_ fields - is_ptr
- is_
re_ exported - is_ref
- is_
slice - is_
strict_ ty - is_
strict_ ty_ convert - is_
verify_ target_ func - Filter the function which contains “rapx::proof”
- match_
primitive_ 🔒type - Match built-in primitive types from String
- match_
std_ unsafe_ callee - match_
std_ unsafe_ chains_ callee - match_
ty_ with_ ident - Match a type identifier string to a concrete Rust type
- parse_
cis_ local - Parse attr.expr into local id and local fields.
- parse_
expr_ into_ local_ and_ ty - parse single expr into (local, fields, ty)
- parse_
expr_ into_ number - parse expr into number.
- parse_
local_ signature - Return the Vecs of args’ names and types of local functions.
- parse_
outside_ 🔒signature - Return the Vecs of args’ names and types of outside functions.
- parse_
signature - Return the Vecs of args’ names and types This function will handle outside def_id by different way.
- print_
hashset - print_
unsafe_ chains - reflect_
generic - reverse_
op - try_
get_ 🔒mir