Function generate_contract_from_annotation 

pub fn generate_contract_from_annotation<'tcx>(
    tcx: TyCtxt<'tcx>,
    def_id: DefId,
) -> Vec<(usize, Vec<(usize, Ty<'tcx>)>, PropertyContract<'tcx>)>

Get the annotation in tag-std style. Then generate contract facts 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)>