C Semantics in K Framework

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

Sure-- I thought you might be talking about some sort of C-level problem.

In practice, it's almost certainly never a good idea to read device 
registers in unspecified order.  Some embedded compilers warn about this. 
Providing robust checking for this would be a very good use of kcc.

John




On 06/23/2011 02:26 PM, Derek M Jones wrote:
> John,
>
> > > > 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?
>
> If the successive characters on the input port that both v1 and v2
> happen to map to are '1' and '2' then the result of the subtraction
> will depend on which of the two operands is evaluated (ie reads from
> the input port) first.