From 61c433a8de1af16d7f872230c1fff34c0ce0d355 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 28 Feb 2023 19:54:49 -0800 Subject: [PATCH] Fix regression with stub external resolve (#2248) I just noticed a regression on https://github.com/model-checking/kani/pull/2227 where I incorrectly updated a test that should've caught this regression. Thus, fix the issue and revert the changes to the test. --- kani-compiler/src/kani_middle/resolve.rs | 21 ++++++++++++------- .../stubbing-validate-random/main.expected | 2 +- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index bd6008246c93..cb36ec1ef32d 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -193,15 +193,20 @@ fn resolve_prefix<'tcx>( segments.next(); resolve_super(tcx, current_module, segments) } + SUPER => resolve_super(tcx, current_module, segments), _ => { - let path = resolve_super(tcx, current_module, segments)?; - if !path.segments.is_empty() { - let next_name = path.segments.first().unwrap(); - let def_id = resolve_in_module(tcx, path.base, &next_name)?; - Ok(Path { base: def_id, segments: Vec::from(&path.segments[1..]) }) - } else { - Ok(path) - } + // No special key word was used. Try local first otherwise try external name. + let next_name = segments.next().unwrap(); + let def_id = + resolve_in_module(tcx, current_module.to_def_id(), &next_name).or_else(|err| { + if matches!(err, ResolveError::MissingItem { .. }) { + // Only try external if we couldn't find anything. + resolve_external(tcx, &next_name).ok_or(err) + } else { + Err(err) + } + })?; + Ok(Path { base: def_id, segments: segments.collect() }) } } } diff --git a/tests/cargo-kani/stubbing-validate-random/main.expected b/tests/cargo-kani/stubbing-validate-random/main.expected index 9a8baf6c9488..34c886c358cb 100644 --- a/tests/cargo-kani/stubbing-validate-random/main.expected +++ b/tests/cargo-kani/stubbing-validate-random/main.expected @@ -1 +1 @@ -error: failed to resolve `rand::random`: unable to find `rand` inside module `stubbing_validate_random` +VERIFICATION:- SUCCESSFUL