@@ -148,20 +148,32 @@ class UnsafeCast extends Cast {
148
148
* 1. the result of `(T)x` is compatible with the type `T` for any `T`
149
149
* 2. the result of `(T)x` is compatible with the type `U` for any `U` such
150
150
* that `U` is a subtype of `T`, or `T` is a subtype of `U`.
151
- * 3. the result of `(T)x` is compatible with the type `U` if `U` the list
151
+ * 3. the result of `(T)x` is compatible with the type `U` if the list
152
+ * of fields of `T` is a prefix of the list of fields of `U`.
153
+ * For example, if `U` is `struct { unsigned char x; int y; };`
154
+ * and `T` is `struct { unsigned char uc; };`.
155
+ * 4. the result of `(T)x` is compatible with the type `U` if the list
152
156
* of fields of `U` is a prefix of the list of fields of `T`.
153
- * For example, if `T` is `struct { unsigned char x; int y; };`
154
- * and `U` is `struct { unsigned char uc; };`.
157
+ *
158
+ * Condition 4 is a bit controversial, since it assumes that the additional
159
+ * fields in `T` won't be accessed. This may result in some FNs.
155
160
*/
156
161
bindingset [ this , t]
157
162
pragma [ inline_late]
158
163
predicate compatibleWith ( Type t ) {
164
+ // Conition 1
159
165
t .stripType ( ) = this .getConvertedType ( )
160
166
or
167
+ // Condition 3
161
168
prefix ( this .getConvertedType ( ) , t .stripType ( ) )
162
169
or
170
+ // Condition 4
171
+ prefix ( t .stripType ( ) , this .getConvertedType ( ) )
172
+ or
173
+ // Condition 2 (a)
163
174
t .stripType ( ) .( Class ) .getABaseClass + ( ) = this .getConvertedType ( )
164
175
or
176
+ // Condition 2 (b)
165
177
t .stripType ( ) = this .getConvertedType ( ) .getABaseClass + ( )
166
178
}
167
179
}
0 commit comments