C Semantics in K Framework

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

Chucky,

> I think an analysis of volatile variables is more useful.  As John
> points out, volatiles are poorly handled by compilers

Your tool is developer oriented not compiler oriented.

> (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).

restrict is useful in that it tells us something about
developer beliefs about their code.  It would be very useful
to know when these beliefs are incorrect.

Compilers are still catching up on how they might make use
of restrict, just like years ago they did not do must with
the register storage class.

--
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