Skip to content

memOutOfBounds analysis causes integer overflow #1801

Description

@Robotechnic

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.

Metadata

Metadata

Assignees

Type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions