Unsoundness for `malloc(0)`

[michael-schwarz]

The C standard says:

If the size of the space requested is zero, the behavior is implementation defined: either a null pointer is returned, or the behavior is as if the size were some nonzero value, except that the returned pointer shall not be used to access an object

-- C99 draft, 7.20.3 (1)

This is independent from the sem.malloc.fail option. GCC does not make a choice here and leaves the decision up to the standard library.

int main(void){
  int* ptr = malloc(0);

  if(ptr == 0) {
    // Reachable
    __goblint_check(1);
  }
}

We report:

[Warning][Deadcode][CWE-570] condition '(unsigned long )ptr == (unsigned long )((int *)0)' is always false (tests/regression/11-heap/17-malloc-zero-bytes.c:6:6-6:14)

[sim642]

I suppose we could have two options to control this behavior:

1. sem.malloc.zero.null - boolean whether malloc(0) may return NULL.
2. sem.malloc.zero.blob - boolean whether malloc(0) may return a (pointer to a) blob of size 0.

This allows Goblint to be configured implementation-defined behaviors which do it one way or the other. Or as an overapproximation account for both.

[michael-schwarz]

Maybe an enum with three options would be the more reasonable thing. With two bools, I can configure it such that neither of these is an option, which is strange.