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
