@@ -36,30 +36,32 @@ int lowerBound(VarAccess va) {
3636 )
3737}
3838
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+
3953/**
4054 * Holds if the index expression is a `VarAccess`, where the variable has been confirmed to be less
4155 * than the length.
4256 */
4357predicate lessthanLength ( ArrayAccess a ) {
44- exists ( ComparisonExpr lessThanLength , VarAccess va |
58+ exists ( ComparisonExpr lessThanLength , VarAccess va , Element qualifier |
4559 va = a .getIndexExpr ( ) and
4660 conditionHolds ( lessThanLength , va )
4761 |
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
5064 lessThanLength .getLesserOperand ( ) = va .getVariable ( ) .getAnAccess ( ) and
5165 lessThanLength .isStrict ( )
5266 )
5367}
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