Previously alpha.security.ArrayBoundV2 produced very spartan bug
reports; this commit ensures that the relevant (and known) details are
reported to the user.

The logic for detecting bugs is not changed, after this commit the
checker will report the same set of issues, but with better messages.

To test the details of the message generation this commit adds a new
test file 'out-of-bounds-diagnostics.c'. Three of the testcases are
added with FIXME notes because they reveal shortcomings of the existing
modeling and bounds checking code. I will try to fix them in separate
follow-up commits.

I thought for a moment that there are some corner cases where the more
specific "may be too large" message is inaccurate, but I realized that
there are no such cases, so we can use the specific message (which is
slightly more helpful for the user).

This reverts commit 979a387.