Checking Array Bounds by Abstract Interpretation and Symbolic Expressions