@@ -36,30 +36,32 @@ int lowerBound(VarAccess va) {
36
36
)
37
37
}
38
38
39
+ /** Gets an access to `e`, which is either a variable or a method. */
40
+ pragma [ nomagic]
41
+ private Expr getAnAccess ( Element e ) {
42
+ result = e .( Variable ) .getAnAccess ( )
43
+ or
44
+ result .( MethodCall ) .getMethod ( ) = e
45
+ }
46
+
47
+ pragma [ nomagic]
48
+ private predicate lengthAccess ( FieldAccess fa , Element qualifier ) {
49
+ fa .getQualifier ( ) = getAnAccess ( qualifier ) and
50
+ fa .getField ( ) .hasName ( "length" )
51
+ }
52
+
39
53
/**
40
54
* Holds if the index expression is a `VarAccess`, where the variable has been confirmed to be less
41
55
* than the length.
42
56
*/
43
57
predicate lessthanLength ( ArrayAccess a ) {
44
- exists ( ComparisonExpr lessThanLength , VarAccess va |
58
+ exists ( ComparisonExpr lessThanLength , VarAccess va , Element qualifier |
45
59
va = a .getIndexExpr ( ) and
46
60
conditionHolds ( lessThanLength , va )
47
61
|
48
- lessThanLength .getGreaterOperand ( ) . ( FieldAccess ) . getQualifier ( ) = arrayReference ( a ) and
49
- lessThanLength . getGreaterOperand ( ) . ( FieldAccess ) . getField ( ) . hasName ( "length" ) and
62
+ lengthAccess ( lessThanLength .getGreaterOperand ( ) , qualifier ) and
63
+ a . getArray ( ) = getAnAccess ( qualifier ) and
50
64
lessThanLength .getLesserOperand ( ) = va .getVariable ( ) .getAnAccess ( ) and
51
65
lessThanLength .isStrict ( )
52
66
)
53
67
}
54
-
55
- /**
56
- * Return all other references to the array accessed in the `ArrayAccess`.
57
- */
58
- pragma [ nomagic]
59
- private Expr arrayReference ( ArrayAccess arrayAccess ) {
60
- // Array is stored in a variable.
61
- result = arrayAccess .getArray ( ) .( VarAccess ) .getVariable ( ) .getAnAccess ( )
62
- or
63
- // Array is returned from a method.
64
- result .( MethodCall ) .getMethod ( ) = arrayAccess .getArray ( ) .( MethodCall ) .getMethod ( )
65
- }
0 commit comments