C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

Okay, I think I see.  You're saying the outer & is in violation,
because its operand is not a function designator, a * expression, or
an lvalue.  It's clearly not the first two, and it's not an lvalue
because the inner &* isn't an lvalue (per para 3).

Thanks,
-Chucky

On Tue, Jan 17, 2012 at 7:32 PM, Derek M Jones 
<derek AT knosof.co.uk>
 wrote:
> 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
> _______________________________________________
> c-semantics mailing list
> c-semantics AT cs.illinois.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics