C Semantics in K Framework

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

> > Also, is it undefined to have unsequenced reads from two different
> > volatiles?  E.g.,
> > volatile int v1 = 0, v2 = 0;
> > v1 + v2;
>
> Subtraction is more of a problem if they both map to the same input
> device.

I don't see the problem with subtraction and the same input device, can 
you explain?

John