C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

My mistake, I misread the program.  I do this pretty often.  If only
we had formal tools that could explain the meanings of programs to
us...

I could only handle the 99 program if I had some kind of way of
letting the user give volatile values as inputs.  I'll have to think
more about this.

I think an analysis of volatile variables is more useful.  As John
points out, volatiles are poorly handled by compilers
(http://www.cs.utah.edu/~regehr/papers/emsoft08-preprint.pdf).  Also,
the restrict keyword doesn't really seem to help
(http://www.cs.pitt.edu/%7Emock/papers/clei2004.pdf).

-Chucky

On Thu, Jun 23, 2011 at 3:53 PM, Derek M Jones 
<derek AT knosof.co.uk>
 wrote:
> 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
> _______________________________________________
> c-semantics mailing list
> c-semantics AT cs.illinois.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics
>