@@ -104,7 +104,10 @@ impl<'tcx> GotocHook<'tcx> for Assume {
104
104
let loc = tcx. codegen_span_option2 ( span) ;
105
105
106
106
Stmt :: block (
107
- vec ! [ Stmt :: assume( cond, loc. clone( ) ) , Stmt :: goto( tcx. find_label( & target) , loc. clone( ) ) ] ,
107
+ vec ! [
108
+ Stmt :: assume( cond, loc. clone( ) ) ,
109
+ Stmt :: goto( tcx. current_fn( ) . find_label( & target) , loc. clone( ) ) ,
110
+ ] ,
108
111
loc,
109
112
)
110
113
}
@@ -132,7 +135,7 @@ impl<'tcx> GotocHook<'tcx> for Nondet {
132
135
let target = target. unwrap ( ) ;
133
136
let pt = tcx. place_ty ( & p) ;
134
137
if pt. is_unit ( ) {
135
- Stmt :: goto ( tcx. find_label ( & target) , loc)
138
+ Stmt :: goto ( tcx. current_fn ( ) . find_label ( & target) , loc)
136
139
} else {
137
140
let pe = tcx. codegen_place ( & p) . goto_expr ;
138
141
Stmt :: block (
@@ -143,7 +146,7 @@ impl<'tcx> GotocHook<'tcx> for Nondet {
143
146
None => Stmt :: skip( loc. clone( ) ) ,
144
147
Some ( f) => Stmt :: assume( f. call( vec![ pe. address_of( ) ] ) , loc. clone( ) ) ,
145
148
} ,
146
- Stmt :: goto( tcx. find_label( & target) , loc. clone( ) ) ,
149
+ Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , loc. clone( ) ) ,
147
150
] ,
148
151
loc,
149
152
)
@@ -229,7 +232,7 @@ impl<'tcx> GotocHook<'tcx> for Intrinsic {
229
232
Stmt :: block (
230
233
vec ! [
231
234
tcx. codegen_intrinsic( instance, fargs, & p, span) ,
232
- Stmt :: goto( tcx. find_label( & target) , loc. clone( ) ) ,
235
+ Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , loc. clone( ) ) ,
233
236
] ,
234
237
loc,
235
238
)
@@ -263,7 +266,7 @@ impl<'tcx> GotocHook<'tcx> for MemReplace {
263
266
let place_layout = tcx. layout_of ( place_type) ;
264
267
let place_is_zst = place_layout. is_zst ( ) ;
265
268
if place_is_zst {
266
- Stmt :: block ( vec ! [ Stmt :: goto( tcx. find_label( & target) , loc. clone( ) ) ] , loc)
269
+ Stmt :: block ( vec ! [ Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , loc. clone( ) ) ] , loc)
267
270
} else {
268
271
let dest = fargs. remove ( 0 ) ;
269
272
let src = fargs. remove ( 0 ) ;
@@ -273,7 +276,7 @@ impl<'tcx> GotocHook<'tcx> for MemReplace {
273
276
. goto_expr
274
277
. assign( dest. clone( ) . dereference( ) . with_location( loc. clone( ) ) , loc. clone( ) ) ,
275
278
dest. dereference( ) . assign( src, loc. clone( ) ) ,
276
- Stmt :: goto( tcx. find_label( & target) , loc. clone( ) ) ,
279
+ Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , loc. clone( ) ) ,
277
280
] ,
278
281
loc,
279
282
)
@@ -336,7 +339,7 @@ impl<'tcx> GotocHook<'tcx> for MemSwap {
336
339
Stmt :: block (
337
340
vec ! [
338
341
tcx. find_function( & func_name) . unwrap( ) . call( vec![ x, y] ) . as_stmt( loc. clone( ) ) ,
339
- Stmt :: goto( tcx. find_label( & target) , loc. clone( ) ) ,
342
+ Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , loc. clone( ) ) ,
340
343
] ,
341
344
loc,
342
345
)
@@ -374,7 +377,7 @@ impl<'tcx> GotocHook<'tcx> for PtrRead {
374
377
tcx. codegen_place( & p)
375
378
. goto_expr
376
379
. assign( src. dereference( ) . with_location( loc. clone( ) ) , loc. clone( ) ) ,
377
- Stmt :: goto( tcx. find_label( & target) , loc. clone( ) ) ,
380
+ Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , loc. clone( ) ) ,
378
381
] ,
379
382
loc,
380
383
)
@@ -410,7 +413,7 @@ impl<'tcx> GotocHook<'tcx> for PtrWrite {
410
413
Stmt :: block (
411
414
vec ! [
412
415
dst. dereference( ) . assign( src, loc. clone( ) ) . with_location( loc. clone( ) ) ,
413
- Stmt :: goto( tcx. find_label( & target) , loc. clone( ) ) ,
416
+ Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , loc. clone( ) ) ,
414
417
] ,
415
418
loc,
416
419
)
@@ -446,7 +449,7 @@ impl<'tcx> GotocHook<'tcx> for RustAlloc {
446
449
. cast_to( Type :: unsigned_int( 8 ) . to_pointer( ) ) ,
447
450
loc,
448
451
) ,
449
- Stmt :: goto( tcx. find_label( & target) , Location :: none( ) ) ,
452
+ Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , Location :: none( ) ) ,
450
453
] ,
451
454
Location :: none ( ) ,
452
455
)
@@ -482,7 +485,7 @@ impl<'tcx> GotocHook<'tcx> for RustDealloc {
482
485
BuiltinFn :: Free
483
486
. call( vec![ ptr. cast_to( Type :: void_pointer( ) ) ] , loc. clone( ) )
484
487
. as_stmt( loc. clone( ) ) ,
485
- Stmt :: goto( tcx. find_label( & target) , Location :: none( ) ) ,
488
+ Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , Location :: none( ) ) ,
486
489
] ,
487
490
loc,
488
491
)
@@ -524,7 +527,7 @@ impl<'tcx> GotocHook<'tcx> for RustRealloc {
524
527
. cast_to( Type :: unsigned_int( 8 ) . to_pointer( ) ) ,
525
528
loc. clone( ) ,
526
529
) ,
527
- Stmt :: goto( tcx. find_label( & target) , loc. clone( ) ) ,
530
+ Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , loc. clone( ) ) ,
528
531
] ,
529
532
loc,
530
533
)
@@ -560,7 +563,7 @@ impl<'tcx> GotocHook<'tcx> for RustAllocZeroed {
560
563
. cast_to( Type :: unsigned_int( 8 ) . to_pointer( ) ) ,
561
564
loc. clone( ) ,
562
565
) ,
563
- Stmt :: goto( tcx. find_label( & target) , loc. clone( ) ) ,
566
+ Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , loc. clone( ) ) ,
564
567
] ,
565
568
loc,
566
569
)
@@ -601,7 +604,7 @@ impl<'tcx> GotocHook<'tcx> for SliceFromRawPart {
601
604
loc. clone ( ) ,
602
605
)
603
606
. with_location ( loc. clone ( ) ) ;
604
- Stmt :: block ( vec ! [ code, Stmt :: goto( tcx. find_label( & target) , loc. clone( ) ) ] , loc)
607
+ Stmt :: block ( vec ! [ code, Stmt :: goto( tcx. current_fn ( ) . find_label( & target) , loc. clone( ) ) ] , loc)
605
608
}
606
609
}
607
610
0 commit comments