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.