File tree Expand file tree Collapse file tree 2 files changed +10
-7
lines changed
kani-compiler/src/codegen_cprover_gotoc Expand file tree Collapse file tree 2 files changed +10
-7
lines changed Original file line number Diff line number Diff line change 55
66use crate :: codegen_cprover_gotoc:: GotocCtx ;
77use cbmc:: goto_program:: Location ;
8- use rustc_middle:: mir:: { Local , VarDebugInfo , VarDebugInfoContents } ;
8+ use rustc_middle:: mir:: { Local , VarDebugInfoContents } ;
99use rustc_smir:: rustc_internal;
1010use rustc_span:: Span ;
11+ use stable_mir:: mir:: VarDebugInfo ;
1112
1213impl < ' tcx > GotocCtx < ' tcx > {
1314 pub fn codegen_span ( & self , sp : & Span ) -> Location {
@@ -43,10 +44,12 @@ impl<'tcx> GotocCtx<'tcx> {
4344 sp. map_or ( Location :: none ( ) , |x| self . codegen_span ( & x) )
4445 }
4546
46- pub fn find_debug_info ( & self , l : & Local ) -> Option < & VarDebugInfo < ' tcx > > {
47- self . current_fn ( ) . mir ( ) . var_debug_info . iter ( ) . find ( |info| match info. value {
48- VarDebugInfoContents :: Place ( p) => p. local == * l && p. projection . len ( ) == 0 ,
49- VarDebugInfoContents :: Const ( _) => false ,
50- } )
47+ pub fn find_debug_info ( & self , l : & Local ) -> Option < VarDebugInfo > {
48+ rustc_internal:: stable ( self . current_fn ( ) . mir ( ) . var_debug_info . iter ( ) . find ( |info| {
49+ match info. value {
50+ VarDebugInfoContents :: Place ( p) => p. local == * l && p. projection . len ( ) == 0 ,
51+ VarDebugInfoContents :: Const ( _) => false ,
52+ }
53+ } ) )
5154 }
5255}
Original file line number Diff line number Diff line change @@ -22,7 +22,7 @@ impl<'tcx> GotocCtx<'tcx> {
2222 pub fn codegen_var_base_name ( & self , l : & Local ) -> String {
2323 match self . find_debug_info ( l) {
2424 None => format ! ( "var_{}" , l. index( ) ) ,
25- Some ( info) => format ! ( "{}" , info. name) ,
25+ Some ( info) => info. name ,
2626 }
2727 }
2828
You can’t perform that action at this time.
0 commit comments