From 01bf411b514836a25dc5a2f44b6b0cfbaeacfc36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=C4=9Fuz=20A=C4=9Fcayaz=C4=B1?= Date: Fri, 8 Dec 2023 05:10:08 +0300 Subject: [PATCH] Stabilize `find_debug_info` (#2912) Last time we stabilized https://github.com/model-checking/kani/pull/2882, this continues the trend and stabilizes `find_debug_info` as well. --- .../src/codegen_cprover_gotoc/codegen/span.rs | 15 +++++++++------ .../src/codegen_cprover_gotoc/utils/names.rs | 2 +- 2 files changed, 10 insertions(+), 7 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, + } + })) } } 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, } }