memOutOfBounds analysis causes integer overflow
On the following code with the last version of Goblint and --ana.int.interval_set true:
#include <stdlib.h>
int main() {
int **buffer;
buffer = malloc(5 * sizeof(int *));
for (int i = 0; i < 5; i++) {
for (int j = 0; j < 5; j++) {
int x = i * 5 + j;
buffer[i][j] = x;
}
}
return 0;
}
I don't encounter any issues apart from a May dereference NULL pointer warning. However, if I add --set "ana.activated[+]" memOutOfBounds, then I get integer overflow errors on line 11 (buffer[i][j] = x;).
This is not the same issue as in #1767 because here it was a return value problem.
We've added executing_speculative_computations in many places, but not to memOutOfBounds, which unfortunately duplicates a lot of the logic on pointer arithmetic, etc.
However, I think this shouldn't be a problem for us in SV-COMP because valid-memsafety and no-overflow are separate properties. And we shouldn't be activating memOutOfBounds for no-overflow analysis anyway. This is probably why we haven't noticed the spurious warnings in SV-COMP runs.