Derek M Jones
derek at knosof.co.uk
Thu Jun 23 13:47:45 CDT 2011
> 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)
> 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
> 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?
> 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
More information about the c-semantics