There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
VCC should check memory initialization for reads of concrete locations
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.