@@ -148,20 +148,32 @@ class UnsafeCast extends Cast {
148148 * 1. the result of `(T)x` is compatible with the type `T` for any `T`
149149 * 2. the result of `(T)x` is compatible with the type `U` for any `U` such
150150 * 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
152156 * 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.
155160 */
156161 bindingset [ this , t]
157162 pragma [ inline_late]
158163 predicate compatibleWith ( Type t ) {
164+ // Conition 1
159165 t .stripType ( ) = this .getConvertedType ( )
160166 or
167+ // Condition 3
161168 prefix ( this .getConvertedType ( ) , t .stripType ( ) )
162169 or
170+ // Condition 4
171+ prefix ( t .stripType ( ) , this .getConvertedType ( ) )
172+ or
173+ // Condition 2 (a)
163174 t .stripType ( ) .( Class ) .getABaseClass + ( ) = this .getConvertedType ( )
164175 or
176+ // Condition 2 (b)
165177 t .stripType ( ) = this .getConvertedType ( ) .getABaseClass + ( )
166178 }
167179}
0 commit comments