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)