@@ -261,6 +261,12 @@ module AbstractValues {
261261
262262private import AbstractValues
263263
264+ pragma [ nomagic]
265+ private predicate typePattern ( PatternMatch pm , TypePatternExpr tpe , Type t ) {
266+ tpe = pm .getPattern ( ) and
267+ t = pm .getExpr ( ) .getType ( )
268+ }
269+
264270/**
265271 * An expression that evaluates to a value that can be dereferenced. That is,
266272 * an expression that may evaluate to `null`.
@@ -337,19 +343,23 @@ class DereferenceableExpr extends Expr {
337343 or
338344 result =
339345 any ( PatternMatch pm |
340- pm .getExpr ( ) = this and
341- if pm .getPattern ( ) instanceof NullLiteral
342- then
346+ this = pm .getExpr ( ) and
347+ (
343348 // E.g. `x is null`
349+ pm .getPattern ( ) instanceof NullLiteral and
344350 isNull = branch
345- else (
351+ or
346352 // E.g. `x is string` or `x is ""`
347- branch = true and isNull = false
353+ not pm .getPattern ( ) instanceof NullLiteral and
354+ branch = true and
355+ isNull = false
348356 or
349- // E.g. `x is string` where `x` has type `string`
350- pm .getPattern ( ) .( TypePatternExpr ) .getCheckedType ( ) = pm .getExpr ( ) .getType ( ) and
351- branch = false and
352- isNull = true
357+ exists ( TypePatternExpr tpe |
358+ // E.g. `x is string` where `x` has type `string`
359+ typePattern ( result , tpe , tpe .getCheckedType ( ) ) and
360+ branch = false and
361+ isNull = true
362+ )
353363 )
354364 )
355365 or
@@ -1248,6 +1258,7 @@ module Internal {
12481258 )
12491259 }
12501260
1261+ pragma [ nomagic]
12511262 private Expr getAnEqualityCheckVal ( Expr e , AbstractValue v , AbstractValue vExpr ) {
12521263 result = getAnEqualityCheck ( e , v , vExpr .getAnExpr ( ) )
12531264 }
0 commit comments