Remove duplicate binop handling from memOutOfBounds

[sim642]

After inspecting the dashboard checks, turns out this also fixes a soundness issue. The previous handling for Mem strangely only covered dereferencing of variables and binops but nothing else.
The extracted tests contain dereferences of other expressions like *(unsigned char *) s and *--(*s0) (this one is wild!).

I think some redundancy/incorrectness might still remain: Mem does two different bounds checks, one doesn't account for offsets of the Mem, the other doesn't account for offsets of the address under Mem. I suspect these should be one combined check to be tried out in a future PR.

[sim642]

This makes no difference to SV-COMP valid-memsafety verdicts but it does slightly change the dashboard checks:

Before\After	Warning	Error	Safe	Unreached
Warning	5843	0	0	0
Error	3	68	0	0
Safe	15	0	17346	0
Unreached	0	0	0	0

I'll look into the cases which change from safe/error into warnings.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.