Consider the new 2-phase memory model

[nunoplopes]

A Two-Phase Infinite/Finite Low-Level Memory Model
Reconciling integer–pointer casts, finite space, and undef at the LLVM IR level of abstraction

CALVIN BECK, University of Pennsylvania, USA
IRENE YOON, University of Pennsylvania, USA
HANXI CHEN, University of Pennsylvania, USA
YANNICK ZAKOWSKI, Inria & LIP (UMR CNRS/ENS Lyon/UCB Lyon1/INRIA), France
STEVE ZDANCEWIC, University of Pennsylvania, USA

https://arxiv.org/pdf/2404.16143

A quick read wasn't enough to understand if this could be implemented in Alive2 and/or useful for int2ptr support.

[nunoplopes]

See also #754, #777, #732

[regehr]

nice. I really like it when authors work hard to make things understandable for people who aren't notation-first sort of thinkers. this seems intuitively appealing, but I only spent about 20 minutes on it.