Am Mittwoch, dem 10.12.2025 um 03:51 +0000 schrieb Krister Walfridsson via Gcc:
> 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?
Are the precise GIMPLE semantics documented somewhere? I would guess that
some notion of provenance would be criticial also for GIMPLE.
Martin
>
> /Krister
