> But in this model, how can you implement malloc? This is not about runtime implementation, it's about how the compiler reasons about pointers to allocated me

> But in this model, how can you implement malloc? This is not about runtime implementation, it's about how the compiler reasons about pointers to allocated memory on a symbolic level. It just means the compiler would consider all memory accessed through the pointer (and other pointers computed from it) other than the pointed (allocated) memory block to be undefined. Even if this was about runtime behavior, a basic malloc would fulfill this requirement with no changes. It returns a pointer to the allocated block and this pointer itself is the "memory block ID". So absolutely no change, with a reasonable assumption that successive allocations (without freeing in between) always return a different pointer. The compiler could simply generate fat pointers with allocation base address + offset to actual location.