@@ -703,8 +703,10 @@ impl<'tcx> GotocCtx<'tcx> {
703
703
if meta. typ ( ) . sizeof ( & self . symbol_table ) == 0 {
704
704
data_cast
705
705
} else {
706
- let vtable_expr =
707
- meta. member ( "_vtable_ptr" , & self . symbol_table ) . cast_to (
706
+ let vtable_expr = meta
707
+ . member ( "_vtable_ptr" , & self . symbol_table )
708
+ . member ( "pointer" , & self . symbol_table )
709
+ . cast_to (
708
710
typ. lookup_field_type ( "vtable" , & self . symbol_table ) . unwrap ( ) ,
709
711
) ;
710
712
dynamic_fat_ptr ( typ, data_cast, vtable_expr, & self . symbol_table )
@@ -835,13 +837,29 @@ impl<'tcx> GotocCtx<'tcx> {
835
837
dst_goto_typ. lookup_components ( & self . symbol_table ) . unwrap ( ) ;
836
838
assert_eq ! ( dst_components. len( ) , 2 ) ;
837
839
assert_eq ! ( dst_components[ 0 ] . name( ) , "_vtable_ptr" ) ;
838
- assert ! ( dst_components[ 0 ] . typ( ) . is_pointer ( ) ) ;
840
+ assert ! ( dst_components[ 0 ] . typ( ) . is_struct_like ( ) ) ;
839
841
assert_eq ! ( dst_components[ 1 ] . name( ) , "_phantom" ) ;
840
842
self . assert_is_rust_phantom_data_like ( & dst_components[ 1 ] . typ ( ) ) ;
843
+ // accessing pointer type of _vtable_ptr, which is wrapped in NonNull
844
+ let vtable_ptr_typ = dst_goto_typ
845
+ . lookup_field_type ( "_vtable_ptr" , & self . symbol_table )
846
+ . unwrap ( )
847
+ . lookup_components ( & self . symbol_table )
848
+ . unwrap ( ) [ 0 ]
849
+ . typ ( ) ;
841
850
Expr :: struct_expr (
842
- dst_goto_typ,
851
+ dst_goto_typ. clone ( ) ,
843
852
btree_string_map ! [
844
- ( "_vtable_ptr" , vtable_expr. cast_to( dst_components[ 0 ] . typ( ) ) ) ,
853
+ (
854
+ "_vtable_ptr" ,
855
+ Expr :: struct_expr_from_values(
856
+ dst_goto_typ
857
+ . lookup_field_type( "_vtable_ptr" , & self . symbol_table)
858
+ . unwrap( ) ,
859
+ vec![ vtable_expr. clone( ) . cast_to( vtable_ptr_typ) ] ,
860
+ & self . symbol_table
861
+ )
862
+ ) ,
845
863
(
846
864
"_phantom" ,
847
865
Expr :: struct_expr(
0 commit comments