Incorrect model of calloc with respect to memory safety

[shaobo-he]

When the size argument of calloc is 0, it should return a pointer without triggering any memory-safety issues whereas SMACK reports memory safety violations. This is because we do a memset to the malloced pointer which can be 0 when the size is 0 whereas memset is checked for valid pointer dereference. The following is a reproduction,

#include <stdlib.h>
int main() {
  int *a = calloc(0, sizeof(int));
  free(a);
  return 0;
}

Invoking SMACK with --memory-safety produces an error.

[shaobo-he]

This is fixed by #853, which changes how a size-zero allocation is modelled rather than special-casing memset.

Running the repro from the issue description verbatim, smack i586.c --check=memory-safety --verifier=corral:

--mem-mod	develop @ 9dca4d9	#853
no-reuse-impls	error	verified
reuse	error	verified
no-reuse	error	verified

calloc(0, n) calls malloc(0) and then memset(p, 0, 0). The memset was never the problem: a zero-length memset touches no byte and its check passes for any valid pointer. What failed was the pointer. Under the default model $$alloc only assigned its result inside if (n > 0), so for size zero the out-parameter was left unassigned and the program continued with an arbitrary pointer; the other two models returned null. #853 adopts the SV-COMP rule ("allocation never fails"), which selects C11 7.22.3p1's second option, so a size-zero request yields a real, non-null, distinct block of size zero.

test/c/memory-safety/malloc_zero_freed.c on that branch covers calloc(0, 4) alongside malloc(0), and calloc_zero_deref_fail.c pins the other half — the block may not be dereferenced.

Note that #177 remains: calloc can still return null nondeterministically while malloc and alloca never fail.