1
Vote

mistranslation of \unchanged

description

The following gets the warning "pointers of different types (struct S and struct volatile#S) are never equal in pure context" (replacing "\unchanged(p)" with "p==\old(p)" fixes the problem):

typedef struct S S;

typedef struct S {
volatile S *p;
_(invariant \unchanged(p))
} S;

comments

MichalMoskal wrote May 19, 2011 at 5:42 PM

Note that the volatile here makes the entire struct volatile, not the pointer to it. I would be actually happy to kill this feature in VCC, or give a warning about it.

MichalMoskal wrote May 19, 2011 at 5:52 PM

Oh, BTW, the above is not to say that this is not a bug. It is :)

stobies wrote May 20, 2011 at 8:52 AM

I cannot repro the issue with the given example.

MarkHillebrand wrote May 20, 2011 at 10:50 AM

It repros with /3...

Sign in to add a comment or to set email notifications