Skip to content

Commit 3284156

Browse files
committed
bugfix: use def_id_to_vir_path_option when checking external trait_ids, fixes #1425
1 parent e008b9d commit 3284156

File tree

1 file changed

+7
-5
lines changed

1 file changed

+7
-5
lines changed

source/rust_verify/src/rust_to_vir_impl.rs

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
use crate::context::Context;
22
use crate::rust_to_vir_base::{
3-
def_id_to_vir_path, mid_ty_const_to_vir, mid_ty_to_vir, mk_visibility, remove_host_arg,
4-
typ_path_and_ident_to_vir_path,
3+
def_id_to_vir_path, def_id_to_vir_path_option, mid_ty_const_to_vir, mid_ty_to_vir,
4+
mk_visibility, remove_host_arg, typ_path_and_ident_to_vir_path,
55
};
66
use crate::rust_to_vir_func::{check_item_fn, CheckItemFnEither};
77
use crate::util::err_span;
@@ -472,9 +472,11 @@ pub(crate) fn collect_external_trait_impls<'tcx>(
472472
for c in tcx.crates(()) {
473473
assert!(*c != rustc_span::def_id::LOCAL_CRATE);
474474
for trait_id in tcx.traits(*c) {
475-
let path = def_id_to_vir_path(tcx, &ctxt.verus_items, *trait_id);
476-
if all_traits.contains(&path) {
477-
all_trait_ids.push(*trait_id);
475+
let path = def_id_to_vir_path_option(tcx, Some(&ctxt.verus_items), *trait_id);
476+
if let Some(path) = path {
477+
if all_traits.contains(&path) {
478+
all_trait_ids.push(*trait_id);
479+
}
478480
}
479481
}
480482
}

0 commit comments

Comments
 (0)