Function get_struct_invariants_from_annotation 

pub(crate) fn get_struct_invariants_from_annotation<'tcx>(
    tcx: TyCtxt<'tcx>,
    struct_def_id: DefId,
    context_def_id: DefId,
) -> Vec<Property<'tcx>>

Parses struct invariants from source-level RAPx annotations attached to a struct definition.