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())