Function parse_cis_local

Source
pub fn parse_cis_local(
    tcx: TyCtxt<'_>,
    def_id: DefId,
    expr: Vec<Expr>,
) -> (usize, Vec<(usize, Ty<'_>)>)
Expand description

Parse attr.expr into local id and local fields.

Example:

#[rapx::inner(property = ValidPtr(ptr, u32, 1), kind = "precond")]
#[rapx::inner(property = ValidNum(region.size>=0), kind = "precond")]
pub fn xor_secret_region(ptr: *mut u32, region:SecretRegion) -> u32 {...}

The first attribute will be parsed as (1, []). -> “1” means the first arg “ptr”, “[]” means no fields. The second attribute will be parsed as (2, [1]). -> “2” means the second arg “region”, “[1]” means “size” is region’s second field.

If this function doesn’t have args, then it will return default pattern: (0, Vec::new())