pointer comparison in GIMPLE

[Krister Walfridsson]

I have a problem in smtgcc with the semantics of pointer comparison in 
GIMPLE.

Consider the function foo:

   void foo(char *p, long long i)
   {
     char a;
     if (p + i == &a)
       __builtin_abort();
   }

The FRE pass determines that the condition is always false, and the 
if-statement is removed. This is correct in the C semantics, as the only 
way the condition can be true invokes undefined behavior. But GIMPLE is 
more permissive, so p + i may in fact evaluate to the address of a. So 
something else is needed to allow this optimization for GIMPLE.

This could easily be fixed by letting EQ_EXPR evaluate to false for 
pointers with different provenance. But that makes other optimizations 
invalid because then p > q, p == q, and p < q can all be false 
simultaneously.

So I guess I am missing something... Why is this optimization allowed on 
GIMPLE?

    /Krister