Skip to content

Commit

Permalink
Stabilize find_debug_info (#2912)
Browse files Browse the repository at this point in the history
Last time we stabilized
#2882, this continues the
trend and stabilizes `find_debug_info` as well.
  • Loading branch information
ouz-a authored Dec 8, 2023
1 parent 2aca488 commit 01bf411
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 7 deletions.
15 changes: 9 additions & 6 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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<VarDebugInfo> {
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,
}
}))
}
}
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
}
}

Expand Down

0 comments on commit 01bf411

Please sign in to comment.