From a07db3462f5b2ca158bac6002a79fdf1f521981d Mon Sep 17 00:00:00 2001 From: ouz-a Date: Sat, 2 Dec 2023 14:36:25 +0300 Subject: [PATCH 1/2] stabilize `find_debug_info` --- .../src/codegen_cprover_gotoc/codegen/span.rs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 9f88bbbe7b55..3fbfd3629775 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -5,9 +5,10 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Location; -use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents}; +use rustc_middle::mir::{Local, VarDebugInfoContents}; use rustc_smir::rustc_internal; use rustc_span::Span; +use stable_mir::mir::VarDebugInfo; impl<'tcx> GotocCtx<'tcx> { pub fn codegen_span(&self, sp: &Span) -> Location { @@ -43,10 +44,12 @@ impl<'tcx> GotocCtx<'tcx> { sp.map_or(Location::none(), |x| self.codegen_span(&x)) } - pub fn find_debug_info(&self, l: &Local) -> Option<&VarDebugInfo<'tcx>> { - self.current_fn().mir().var_debug_info.iter().find(|info| match info.value { - VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0, - VarDebugInfoContents::Const(_) => false, - }) + pub fn find_debug_info(&self, l: &Local) -> Option { + rustc_internal::stable(self.current_fn().mir().var_debug_info.iter().find(|info| { + match info.value { + VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0, + VarDebugInfoContents::Const(_) => false, + } + })) } } From fb258ebc36fed43b0da77c531abcb7a41a43718d Mon Sep 17 00:00:00 2001 From: ouz-a Date: Wed, 6 Dec 2023 23:04:44 +0300 Subject: [PATCH 2/2] fix clippy warning --- kani-compiler/src/codegen_cprover_gotoc/utils/names.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index 98f6f533cd12..da684b601668 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -22,7 +22,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_var_base_name(&self, l: &Local) -> String { match self.find_debug_info(l) { None => format!("var_{}", l.index()), - Some(info) => format!("{}", info.name), + Some(info) => info.name, } }