[ynik]

The problem is that uninitialized memory really is subtle. After initializing all members of a struct, the padding bytes of that struct are still uninitialized. Yet, it is valid to memcpy the whole struct somewhere else; even with a hand-written char*-based copying loop. (and indeed, this is a good reason for reading uninitialized memory!) So reading uninitialized memory is not always undefined behavior; just most of the time.

The C standard text is barely sufficient for the purposes of compilers, but wholly insufficient for what a model checker would need to know.

[saagarjha]

> After initializing all members of a struct, the padding bytes of that struct are still uninitialized.

Depends on how you initialize them. If you do it all in one go, then yes. If you partially initialize it, then no: some of the padding bytes are guaranteed to be zero. (Observing this and maintaining this variant is an exercise for the reader.)

[o11c]

For reference, GCC has `__builtin_clear_padding` which is very useful to avoid problems there.