@@ -188,7 +188,7 @@ private predicate typePrefixContainsAux1(
188
188
exists ( ParameterizedPrefix pps0 |
189
189
typePrefixContains ( pps0 , ppt0 ) and
190
190
pps = TTypeParam ( pps0 , s ) and
191
- s instanceof Wildcard
191
+ s instanceof Wildcard // manual magic, implied by `typeArgumentContains(_, s, t, _)`
192
192
)
193
193
}
194
194
@@ -197,6 +197,7 @@ private predicate typePrefixContainsAux2(
197
197
ParameterizedPrefix ppt , ParameterizedPrefix ppt0 , RefType s
198
198
) {
199
199
exists ( GenericType g , int n , RefType t |
200
+ // Implies `ppt = TTypeParam(ppt0, t)`
200
201
ppt .split ( g , ppt0 , t , n ) and
201
202
typeArgumentContains ( g , s , t , n )
202
203
)
@@ -268,24 +269,36 @@ private predicate wildcardExtendsObject(Wildcard wc) {
268
269
wc .getUpperBound ( ) .getType ( ) instanceof TypeObject
269
270
}
270
271
271
- private predicate subtypeStarMagic1 ( RefType t ) { t = any ( Wildcard w ) .getUpperBound ( ) .getType ( ) }
272
+ // manual magic for `hasSubtypeStar1`
273
+ private predicate getAWildcardUpperBound ( RefType t ) {
274
+ t = any ( Wildcard w ) .getUpperBound ( ) .getType ( )
275
+ }
272
276
273
- private predicate subtypeStarMagic2 ( RefType t ) { t = any ( Wildcard w ) .getLowerBound ( ) .getType ( ) }
277
+ // manual magic for `hasSubtypeStar2`
278
+ private predicate getAWildcardLowerBound ( RefType t ) {
279
+ t = any ( Wildcard w ) .getLowerBound ( ) .getType ( )
280
+ }
274
281
282
+ /**
283
+ * Holds if `hasSubtype*(t, sub)`, but manuel-magic'ed with `getAWildcardUpperBound(t)`.
284
+ */
275
285
pragma [ nomagic]
276
286
private predicate hasSubtypeStar1 ( RefType t , RefType sub ) {
277
- sub = t and subtypeStarMagic1 ( t )
287
+ sub = t and getAWildcardUpperBound ( t )
278
288
or
279
- hasSubtype ( t , sub ) and subtypeStarMagic1 ( t )
289
+ hasSubtype ( t , sub ) and getAWildcardUpperBound ( t )
280
290
or
281
291
exists ( RefType mid | hasSubtypeStar1 ( t , mid ) and hasSubtype ( mid , sub ) )
282
292
}
283
293
294
+ /**
295
+ * Holds if `hasSubtype*(t, sub)`, but manuel-magic'ed with `getAWildcardLowerBound(sub)`.
296
+ */
284
297
pragma [ nomagic]
285
298
private predicate hasSubtypeStar2 ( RefType t , RefType sub ) {
286
- sub = t and subtypeStarMagic2 ( sub )
299
+ sub = t and getAWildcardLowerBound ( sub )
287
300
or
288
- hasSubtype ( t , sub ) and subtypeStarMagic2 ( sub )
301
+ hasSubtype ( t , sub ) and getAWildcardLowerBound ( sub )
289
302
or
290
303
exists ( RefType mid | hasSubtype ( t , mid ) and hasSubtypeStar2 ( mid , sub ) )
291
304
}
0 commit comments