analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

memOutOfBounds analysis causes integer overflow

Open Robotechnic opened this issue 5 months ago • 1 comments

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.

Robotechnic avatar Aug 04 '25 09:08 Robotechnic

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.

sim642 avatar Aug 04 '25 09:08 sim642