@@ -4,7 +4,7 @@ use super::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
4
4
use super :: cbmc:: utils:: { aggr_name, BUG_REPORT_URL } ;
5
5
use super :: cbmc:: MachineModel ;
6
6
use super :: metadata:: * ;
7
- use super :: typ:: { is_dyn_trait_fat_pointer , is_pointer, pointee_type} ;
7
+ use super :: typ:: { is_pointer, pointee_type} ;
8
8
use super :: utils:: { dynamic_fat_ptr, slice_fat_ptr} ;
9
9
use crate :: btree_string_map;
10
10
use num:: bigint:: BigInt ;
@@ -679,15 +679,18 @@ impl<'tcx> GotocCtx<'tcx> {
679
679
) -> Option < Expr > {
680
680
// Check if the cast is from a vtable fat pointer to another
681
681
// vtable fat pointer (which can happen with auto trait fat pointers)
682
- if is_dyn_trait_fat_pointer ( src_mir_type) {
682
+ if self . is_vtable_fat_pointer ( src_mir_type) {
683
683
self . cast_unsized_dyn_trait_to_unsized_dyn_trait (
684
684
src_goto_expr. clone ( ) ,
685
685
src_mir_type,
686
686
dst_mir_type,
687
687
)
688
688
} else {
689
- // Assert that the source is not a pointer or is a thin pointer
690
- assert ! ( pointee_type( src_mir_type) . map_or( true , |p| self . use_thin_pointer( p) ) ) ;
689
+ // Check that the source is either not a pointer, or a thin or a slice pointer
690
+ assert ! (
691
+ pointee_type( src_mir_type)
692
+ . map_or( true , |p| self . use_thin_pointer( p) || self . use_slice_fat_pointer( p) )
693
+ ) ;
691
694
692
695
// Sized to unsized cast
693
696
self . cast_sized_expr_to_unsized_expr ( src_goto_expr. clone ( ) , src_mir_type, dst_mir_type)
@@ -923,8 +926,8 @@ impl<'tcx> GotocCtx<'tcx> {
923
926
}
924
927
925
928
// The source destination must be a fat pointers to a dyn trait object
926
- assert ! ( is_dyn_trait_fat_pointer ( src_mir_type) ) ;
927
- assert ! ( is_dyn_trait_fat_pointer ( dst_mir_type) ) ;
929
+ assert ! ( self . is_vtable_fat_pointer ( src_mir_type) ) ;
930
+ assert ! ( self . is_vtable_fat_pointer ( dst_mir_type) ) ;
928
931
929
932
let dst_mir_dyn_ty = pointee_type ( dst_mir_type) . unwrap ( ) ;
930
933
@@ -965,7 +968,7 @@ impl<'tcx> GotocCtx<'tcx> {
965
968
966
969
// The src type cannot be a pointer to a dynamic trait object, otherwise
967
970
// we should have called cast_unsized_dyn_trait_to_unsized_dyn_trait
968
- assert ! ( !is_dyn_trait_fat_pointer ( src_mir_type) ) ;
971
+ assert ! ( !self . is_vtable_fat_pointer ( src_mir_type) ) ;
969
972
970
973
match ( src_mir_type. kind ( ) , dst_mir_type. kind ( ) ) {
971
974
( ty:: Ref ( ..) , ty:: Ref ( ..) ) => {
0 commit comments