C Semantics in K Framework

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

Chucky,

> I was writing some tests for this for kcc and hit on the following expression:
> &(&(*(*(void**)NULL))) == (void**)NULL
> I'd argue that based on the standard,&(&(*(*(void**)NULL))) is "as
> if" it were&(*(void**)NULL), which is "as if" it were (void**)NULL.

I disagree.  Operators (and their associated constraints) have to be
applied in a given order.  The exception wording requires that any
constraints still apply before the runtime consequences of &* can be
ignored.  Your code violates the constraints diagnosed by gcc et al.

The following is fine (and not interesting):

&(*(&(*(void**)NULL))) == (void**)NULL

--
Derek M. Jones                  tel: +44 (0) 1252 520 667
Knowledge Software Ltd          blog:shape-of-code.coding-guidelines.com
Source code analysis            http://www.knosof.co.uk