C Semantics in K Framework

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

Chucky,

> I'm going to go ahead and add volatile support to KCC and I thought I
> would get some feedback first.

This could be real hard.  What output does the following produce?

volatile int x;
int y = 0;

while (x != 99)
   y++;

printf("%d", y);

> One thing I'm worried about is that this doesn't address the fact that
> volatile variables can change "behind the scenes".  Would we need a
> way to allow the user to specify how volatiles might change?  I

This is the only interesting aspect of volatile from an analysis
point of view.

> imagine if someone wanted to use KCC to model a device driver, and the
> volatiles changed in particular ways (e.g., a read from volatile loc
> 500 causes a write of 0 at volatile loc 501 behind the scenes), they
> would want this mechanism.

Perhaps a file could contain a list of values and every time
a volatile value was accessed a value could be obtained from
this list.  The list could contain variable+value or a have
different file for every variable.

> Also, is it undefined to have unsequenced reads from two different
> volatiles?  E.g.,
> volatile int v1 = 0, v2 = 0;
> v1 + v2;

Subtraction is more of a problem if they both map to the same input
device.

> I'm wondering since there is that sentence "What constitutes an access
> to an object that has volatile-qualified type is
> implementation-defined."    I've also heard casually that "a volatile
> access can be thought of as a potential access anywhere in memory".  I
> suppose it means "anywhere in volatile memory".  Is this correct?

Sentence 1488.

> Should I worry about this?

If you want to claim correctness you have to worry about everything :-)

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