Function collect_properties_from_ensures_attrs 

fn collect_properties_from_ensures_attrs<'tcx>(
    tcx: TyCtxt<'tcx>,
    attrs: impl IntoIterator<Item = &'tcx Attribute>,
    property_def_id: DefId,
    parse_error_label: &str,
) -> Vec<Property<'tcx>>

Collects properties from #[rapx::ensures(...)] attributes.