pub fn generate_contract_from_annotation(
tcx: TyCtxt<'_>,
def_id: DefId,
) -> Vec<(usize, Vec<(usize, Ty<'_>)>, PropertyContract<'_>)>Expand description
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)>