/* XXX: This is a HACK, and will not work in general! We just use the
* lower 32 bits of the address, and do the same as for the 32-bit
* version. As long as the OS gives us memory in a roughly linear
/* XXX: This is a HACK, and will not work in general! We just use the
* lower 32 bits of the address, and do the same as for the 32-bit
* version. As long as the OS gives us memory in a roughly linear