Spurious warning due to wrong array size from `calloc`

[Robotechnic]

I just found out that this program:

#include <assert.h>
#include <stdlib.h>

int main() {
	int *buff = calloc(50, sizeof(int));
	if (buff == NULL) {
		return 1;
	}
	return buff[5];
}

Causes goblint to raise an error while it shouldn't. I get:

[Error][Behavior > Undefined > ArrayOutOfBounds > PastEnd] Must access array past end

It has been mentioned in #702 and #135, but this is not really a precision problem.

Changing the array size to the number of items and the blob size to the size of each item seems to fix the issue with this particular problem. However, it breaks soundness, so it isn't a suitable solution.

[sim642]

Changing the array size to the number of items and the blob size to the size of each item seems to fix the issue with this particular problem. However, it breaks soundness, so it isn't a suitable solution.

For reference, the result of calloc is currently wrapped into an array of size 1 here:

analyzer/src/analyses/base.ml

Line 2739 in 861891e

(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, ZeroInit.calloc))));

This seems to be some internal hack for achieving soundness, but it has confusing consequences on the output because we seem to check the indexing [5] on that internal array.

[sim642]

Changing the array size to the number of items and the blob size to the size of each item seems to fix the issue with this particular problem. However, it breaks soundness, so it isn't a suitable solution.

I tried tracing this and it leads to another arrays/blobs issue in 11-heap/12-calloc:

  int* arr = calloc(5,sizeof(int));
  arr[0] = 3;
  __goblint_check(arr[2] == 0); //UNKNOWN

Only if we make the array of size 5, arr[2] will read the 3 from the previous assignment and not the initialized 0.
We can't blame this on uninitialized memory either, because here everything is properly initialized. So it's our array/blob domain at fault for just reading the wrong thing.