C Semantics in K Framework

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

volatile is way more useful for programs that I look at.

But I bet restrict is pretty easy to handle, given the machinery you 
already have in place!

John




On 06/23/2011 03:07 PM, Chucky Ellison wrote:
> 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
>
> _______________________________________________
> c-semantics mailing list
> c-semantics AT cs.illinois.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics