Java: Account for additional constants in ArrayIndexOutOfBounds query.

This commit is contained in:
Anders Schack-Mulligen
2022-12-16 11:02:28 +01:00
parent a1aeb995e6
commit 2d6d8aaa74
3 changed files with 18 additions and 0 deletions

View File

@@ -44,6 +44,15 @@ predicate boundedArrayAccess(ArrayAccess aa, int k) {
)
)
)
or
exists(Field arr, Expr index, int delta, int arrlen |
aa.getIndexExpr() = index and
aa.getArray() = arr.getAnAccess() and
bounded(index, any(ZeroBound z), delta, true, _) and
arr.isFinal() and
arr.getInitializer().(ArrayCreationExpr).getFirstDimensionSize() = arrlen and
k = delta - arrlen
)
}
/**