Function get_contract_from_annotation 

pub(crate) fn get_contract_from_annotation<'tcx>(
    tcx: TyCtxt<'tcx>,
    def_id: DefId,
) -> Vec<Property<'tcx>>

Parses requires contracts from source-level RAPx annotations attached to a definition.