Predicate ArrayIndexOutOfBounds::boundedArrayAccess

Holds if the index expression of aa is less than or equal to the array length plus k.

predicate boundedArrayAccess(ArrayAccess aa, int k)