@@ -85,7 +85,7 @@ impl<'tcx> GotocCtx<'tcx> {
85
85
// };
86
86
// ```
87
87
// And notice that its `.pointer` field is exactly what we want.
88
- assert ! ( e. typ( ) . is_rust_box( ) ) ;
88
+ assert ! ( e. typ( ) . is_rust_box( ) , "expected rust box {:?}" , e ) ;
89
89
let unique_ptr_typ =
90
90
self . symbol_table . lookup_field_type_in_type ( e. typ ( ) , "0" ) . unwrap ( ) . clone ( ) ;
91
91
assert ! ( unique_ptr_typ. is_rust_unique_pointer( ) ) ;
@@ -96,7 +96,7 @@ impl<'tcx> GotocCtx<'tcx> {
96
96
/// `boxed_type the_box = >>> { .0=nondet(), .1={ ._marker=nondet(), .pointer=boxed_value } } <<<`
97
97
/// `boxed_type` is the type of the resulting expression
98
98
pub fn box_value ( & self , boxed_value : Expr , boxed_type : Type ) -> Expr {
99
- assert ! ( boxed_type. is_rust_box( ) ) ;
99
+ assert ! ( boxed_type. is_rust_box( ) , "expected rust box {:?}" , boxed_type ) ;
100
100
let get_field_type = |struct_typ, field| {
101
101
self . symbol_table . lookup_field_type_in_type ( struct_typ, field) . unwrap ( ) . clone ( )
102
102
} ;
@@ -119,11 +119,15 @@ impl<'tcx> GotocCtx<'tcx> {
119
119
}
120
120
121
121
impl Type {
122
- /// Checks if the struct represents a Rust "Box"
122
+ /// Best effort check if the struct represents a Rust "Box". May return false positives.
123
123
pub fn is_rust_box ( & self ) -> bool {
124
- self . type_name ( ) . map_or ( false , |name| {
125
- name. starts_with ( "tag-std::boxed::Box" ) || name. starts_with ( "tag-core::boxed::Box" )
126
- } )
124
+ // We have seen variants on the name, including
125
+ // tag-std::boxed::Box, tag-core::boxed::Box, tag-boxed::Box.
126
+ // If we match on exact names, we're playing whack-a-mole trying to keep track of how this
127
+ // can be reimported.
128
+ // If we don't, we spuriously fail. https://github.com/model-checking/rmc/issues/113
129
+ // TODO: find a better way of checking this https://github.com/model-checking/rmc/issues/152
130
+ self . type_name ( ) . map_or ( false , |name| name. contains ( "boxed::Box" ) )
127
131
}
128
132
129
133
/// Checks if the struct represents a Rust "Unique"
0 commit comments