Open michael-schwarz opened 2 months ago
I suppose we could have two options to control this behavior:
sem.malloc.zero.null
- boolean whether malloc(0)
may return NULL
.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.
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.
The C standard says:
-- 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.We report: