File tree 2 files changed +10
-7
lines changed
kani-compiler/src/codegen_cprover_gotoc
2 files changed +10
-7
lines changed Original file line number Diff line number Diff line change 5
5
6
6
use crate :: codegen_cprover_gotoc:: GotocCtx ;
7
7
use cbmc:: goto_program:: Location ;
8
- use rustc_middle:: mir:: { Local , VarDebugInfo , VarDebugInfoContents } ;
8
+ use rustc_middle:: mir:: { Local , VarDebugInfoContents } ;
9
9
use rustc_smir:: rustc_internal;
10
10
use rustc_span:: Span ;
11
+ use stable_mir:: mir:: VarDebugInfo ;
11
12
12
13
impl < ' tcx > GotocCtx < ' tcx > {
13
14
pub fn codegen_span ( & self , sp : & Span ) -> Location {
@@ -43,10 +44,12 @@ impl<'tcx> GotocCtx<'tcx> {
43
44
sp. map_or ( Location :: none ( ) , |x| self . codegen_span ( & x) )
44
45
}
45
46
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
+ } ) )
51
54
}
52
55
}
Original file line number Diff line number Diff line change @@ -22,7 +22,7 @@ impl<'tcx> GotocCtx<'tcx> {
22
22
pub fn codegen_var_base_name ( & self , l : & Local ) -> String {
23
23
match self . find_debug_info ( l) {
24
24
None => format ! ( "var_{}" , l. index( ) ) ,
25
- Some ( info) => format ! ( "{}" , info. name) ,
25
+ Some ( info) => info. name ,
26
26
}
27
27
}
28
28
You can’t perform that action at this time.
0 commit comments