C Semantics in K Framework

[John Regehr <regehr AT cs.utah.edu>]

> I'm wondering since there is that sentence "What constitutes an access
> to an object that has volatile-qualified type is
> implementation-defined."

I should add that I do not know of any C implementations that take 
meaningful advantage of the freedom that this sentence appears to offer.

Such a compiler would likely be useless for embedded systems and 
operating systems.

John