C Semantics in K Framework

[Derek M Jones <derek AT knosof.co.uk>]

Chucky,

> > volatile int x;
> > int y = 0;
> >
> > while (x != 99)
> >     y++;
> >
> > printf("%d", y);
>
> - read of 'unknown' from memory location [wherever x is]
...
> - write of "99" to stdout

Why does y have the value 99?

> I think for the first phase of adding volatiles, all reads would
> return 'unknown'.

Why do you want to do volatile next?  restrict is not as
complicated (on the user interface side) and would be
something of interest to people.

> Why is subtraction more of a problem?  Simply because you could get

See previous reply to John.

> In fact, wouldn't v1 - v1 be undefined?

It ought to be but the wording in the standard does not make it so.

> It looks like you have an example on digital page 279 under sentence 194.
> int a;
> volatile int b, c;
> void f(void)  {
>      int t;
>      a = b + c;
>      a = ((t = b), t + c);
> }
> I assume if you have this example, it isn't undefined; I just don't
> understand how.

There is a sequence point between the evaluation of the two operands
of the comma operator.

> > Sentence 1488.
>
> I can't believe bit fields can be volatile...  I guess it doesn't
> matter since people who use volatiles are probably doing something
> that isn't portable anyway.

There is no rule preventing them from being used on bit fields.
Some processors do have instructions that allow sequences of bits
within a byte/word to be read/written.  Whether this actually maps
onto byte operations internally I have no idea and neither do I
know if anybody builds I/O devices capable of working like this.
But the C Standard is there for them (we do get people turning up at
WG14 meeting with some very odd requests and then never see them
again)!

--
Derek M. Jones                         tel: +44 (0) 1252 520 667
Knowledge Software Ltd                 
mailto:derek AT knosof.co.uk
Source code analysis                   http://www.knosof.co.uk