Skip to content

Commit 61c433a

Browse files
authored
Fix regression with stub external resolve (rust-lang#2248)
I just noticed a regression on model-checking/kani#2227 where I incorrectly updated a test that should've caught this regression. Thus, fix the issue and revert the changes to the test.
1 parent 07a48e6 commit 61c433a

File tree

2 files changed

+14
-9
lines changed

2 files changed

+14
-9
lines changed

kani-compiler/src/kani_middle/resolve.rs

+13-8
Original file line numberDiff line numberDiff line change
@@ -193,15 +193,20 @@ fn resolve_prefix<'tcx>(
193193
segments.next();
194194
resolve_super(tcx, current_module, segments)
195195
}
196+
SUPER => resolve_super(tcx, current_module, segments),
196197
_ => {
197-
let path = resolve_super(tcx, current_module, segments)?;
198-
if !path.segments.is_empty() {
199-
let next_name = path.segments.first().unwrap();
200-
let def_id = resolve_in_module(tcx, path.base, &next_name)?;
201-
Ok(Path { base: def_id, segments: Vec::from(&path.segments[1..]) })
202-
} else {
203-
Ok(path)
204-
}
198+
// No special key word was used. Try local first otherwise try external name.
199+
let next_name = segments.next().unwrap();
200+
let def_id =
201+
resolve_in_module(tcx, current_module.to_def_id(), &next_name).or_else(|err| {
202+
if matches!(err, ResolveError::MissingItem { .. }) {
203+
// Only try external if we couldn't find anything.
204+
resolve_external(tcx, &next_name).ok_or(err)
205+
} else {
206+
Err(err)
207+
}
208+
})?;
209+
Ok(Path { base: def_id, segments: segments.collect() })
205210
}
206211
}
207212
}
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
error: failed to resolve `rand::random`: unable to find `rand` inside module `stubbing_validate_random`
1+
VERIFICATION:- SUCCESSFUL

0 commit comments

Comments
 (0)