Fix spurious overflow checks in memOutOfBounds

[sim642]

Closes #1801.

This is currently on top of #2077 because it (and some previous memOutOfBounds changes) already remove many of the ID operations from memOutOfBounds.

[michael-schwarz]

This should come with a regression test.

[sim642]

This should come with a regression test.

The example in #1801 is actually already solved by some other PR which removed the corresponding ID operation in memOutOfBounds.

Adding tests for the remaining instances fixes in this PR turned out to be surprisingly difficult because the multiplication case involves array length, which CIL still returns as OCaml int (and throws otherwise), which implicitly sets a bound.
Luckily with a large-enough array element size the overflow still happens (and the warning is removed by this PR).

The size multiplication overflowing to top has an interesting consequence though: according to the interval, the size of something may also be negative. But I'm not sure it'd even make a difference to refine it to be non-negative: it could still be 0, so access at index 0 would be invalid, and access at negative index would be invalid anyway.

[sim642]

These reveal unsoundness in memOutOfBounds. I think we just happen to be covered by ana.arrayoob for these very basic things, but there's no reason why memOutOfBounds shouldn't be able to handle these correctly.

[michael-schwarz]

I think it was a deliberate choice to use ana.arrayoob for this.

[sim642]

It's hard to draw the line between that ana.arrayoob is supposed to do and what memOutOfBounds is supposed to do. And it's even harder to make sure that they actually cover everything with such a split.

I think memOutOfBounds should still be able to warn about these because it needs to be able to do the simple stuff anyway. Trying to avoid that and only handling the complex stuff is probably what makes memOutOfBounds so involved and error-prone.

ana.arrayoob also shoots us in the foot a lot with the single-element calloc arrays: #1766. Potentially all of memOutOfBounds could be done in base directly, like ana.arrayoob but that would just make base even more complicated.
We could still keep ana.arrayoob around but not use it with memOutOfBounds (if it did handle this stuff).