Skip to content

Commit d350c4a

Browse files
committed
Fix span lookup for function signature during erasure
1 parent 96c613f commit d350c4a

File tree

2 files changed

+5
-5
lines changed

2 files changed

+5
-5
lines changed

verify/rust_verify/src/erase.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -274,13 +274,13 @@ fn erase_block(ctxt: &Ctxt, is_exec: bool, block: &Block) -> Block {
274274
Block { stmts, id, rules, span, tokens: block.tokens.clone() }
275275
}
276276

277-
fn erase_fn(ctxt: &Ctxt, f_span: &Span, f: &FnKind) -> Option<FnKind> {
278-
let f_vir = &ctxt.functions_by_span[f_span];
277+
fn erase_fn(ctxt: &Ctxt, f: &FnKind) -> Option<FnKind> {
278+
let FnKind(defaultness, sig, generics, body_opt) = f;
279+
let f_vir = &ctxt.functions_by_span[&sig.span];
279280
match f_vir.x.mode {
280281
Mode::Spec | Mode::Proof => return None,
281282
Mode::Exec => {}
282283
}
283-
let FnKind(defaultness, sig, generics, body_opt) = f;
284284
let FnSig { header: _, decl, span: _ } = sig;
285285
let FnDecl { inputs, output } = &**decl;
286286
let mut new_inputs: Vec<Param> = Vec::new();
@@ -318,7 +318,7 @@ fn erase_item(ctxt: &Ctxt, item: &Item) -> Vec<P<Item>> {
318318
if vattrs.external {
319319
return vec![P(item.clone())];
320320
}
321-
match erase_fn(ctxt, &item.span, kind) {
321+
match erase_fn(ctxt, kind) {
322322
None => return vec![],
323323
Some(kind) => ItemKind::Fn(Box::new(kind)),
324324
}

verify/rust_verify/src/rust_to_vir.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ use crate::util::unsupported_err_span;
1414
use crate::{err_unless, unsupported_err, unsupported_err_unless, unsupported_unless};
1515
use rustc_ast::Attribute;
1616
use rustc_hir::{
17-
AssocItemKind, Crate, ForeignItem, ForeignItemId, ForeignItemKind, HirId, ImplItemKind, Item,
17+
Crate, ForeignItem, ForeignItemId, ForeignItemKind, HirId, Item,
1818
ItemId, ItemKind, ModuleItems, QPath, TraitRef, TyKind,
1919
};
2020
use rustc_middle::ty::TyCtxt;

0 commit comments

Comments
 (0)