@@ -142,6 +142,7 @@ private module GuardsInput implements
142142 }
143143 }
144144
145+ pragma [ nomagic]
145146 predicate equalityTest ( Expr eqtest , Expr left , Expr right , boolean polarity ) {
146147 exists ( ComparisonTest ct |
147148 ct .getExpr ( ) = eqtest and
@@ -410,6 +411,22 @@ private predicate typePattern(PatternMatch pm, TypePatternExpr tpe, Type t) {
410411 t = pm .getExpr ( ) .getType ( )
411412}
412413
414+ pragma [ nomagic]
415+ private predicate dereferenceableExpr ( Expr e , boolean isNullableType ) {
416+ exists ( Type t | t = e .getType ( ) |
417+ t instanceof NullableType and
418+ isNullableType = true
419+ or
420+ t instanceof RefType and
421+ isNullableType = false
422+ )
423+ or
424+ exists ( Expr parent |
425+ dereferenceableExpr ( parent , isNullableType ) and
426+ e = getNullEquivParent ( parent )
427+ )
428+ }
429+
413430/**
414431 * An expression that evaluates to a value that can be dereferenced. That is,
415432 * an expression that may evaluate to `null`.
@@ -418,21 +435,12 @@ class DereferenceableExpr extends Expr {
418435 private boolean isNullableType ;
419436
420437 DereferenceableExpr ( ) {
421- exists ( Expr e , Type t |
422- // There is currently a bug in the extractor: the type of `x?.Length` is
423- // incorrectly `int`, while it should have been `int?`. We apply
424- // `getNullEquivParent()` as a workaround
425- this = getNullEquivParent * ( e ) and
426- t = e .getType ( ) and
427- not this instanceof SwitchCaseExpr and
428- not this instanceof PatternExpr
429- |
430- t instanceof NullableType and
431- isNullableType = true
432- or
433- t instanceof RefType and
434- isNullableType = false
435- )
438+ // There is currently a bug in the extractor: the type of `x?.Length` is
439+ // incorrectly `int`, while it should have been `int?`. We apply
440+ // `getNullEquivParent()` as a workaround
441+ dereferenceableExpr ( this , isNullableType ) and
442+ not this instanceof SwitchCaseExpr and
443+ not this instanceof PatternExpr
436444 }
437445
438446 /** Holds if this expression has a nullable type `T?`. */
0 commit comments