1
Vote

VCC should check memory initialization for reads of concrete locations

description

VCC doesn't check that memory that is read has been initialized. While this feature is useful for ghost memory (it provides a convenient encoding of nondeterministic choice), standard C mandates that reading uninitialized memory results in undefined behavior, and modern compilers take advantage of this. The requirement should be enforced for all concrete locations.

comments